6.126 One can figure out whether a proposition belongs to logic by figuring out the logical properties of symbols.

And this is what we do when we “prove” a logical proposition. Because without concerning ourselves with a sense [Sinn] and a meaning [Bedeutung] we construct the logical proposition from others according to mere rules for signs.

The proof of a logical proposition consists in our being able to establish it from other logical propositions with successive applications of certain operations, which produce ever more tautologies from the first one. (In fact from a tautology only tautologies follow.)

Of course this way of showing that its propositions are tautologies is thoroughly inessential to logic. Because the propositions, from which the proof starts out, must show, indeed without proof, that they are tautologies.

Logic is, or belongs to, a system that cannot justify itself.

Frascolla (p. 141): “If we take the expression ‘logical proof’ in its more general meaning, and if we call ‘mechanical’ any procedure of calculation, understood as a set of effective instructions for manipulating symbols, then in the light of Church’s Theorem of Undecidability of the first-order predicative calculus, Wittgenstein’s thesis is simply false, since no mechanical procedure can exist which enables us to decide, given any arbitrary formula of the first-order predicative calculus (which is included in the calculus of Principia Mathematica), whether it is a tautology or not.”