Whether a proposition belongs to logic can be calculated by calculating the logical properties of the symbol.

And this we do when we prove a logical proposition. For without troubling ourselves about a sense and a meaning, we form the logical propositions out of others by mere symbolic rules.

We prove a logical proposition by creating it out of other logical propositions by applying in succession certain operations, which again generate tautologies out of the first. (And from a tautology only tautologies follow.)

Naturally this way of showing that its propositions are tautologies is quite unessential to logic. Because the propositions, from which the proof starts, must show without proof that they are tautologies.

6.1261    In logic process and result are equivalent. (Therefore no surprises.)

6.1262    Proof in logic is only a mechanical expedient to facilitate the recognition of tautology, where it is complicated.

6.1263    It would be too remarkable, if one could prove a significant proposition logically from another, and a logical proposition also. It is clear from the beginning that the logical proof of a significant proposition and the proof in logic must be two quite different things.

6.1264    The significant proposition asserts something, and its proof shows that it is so; in logic every proposition is the form of a proof.

Every proposition of logic is a modus ponens present in signs. (And the modus ponens can not be expressed by a proposition.)

6.1265    Logic can always be conceived to be such that every proposition is its own proof.