Propositional Logic, Syntactic Implication

Propo­si­tional Logic

Some Definitions

Propo­si­tional logic is a sim­plified model of what it means to prove things. The state­ments that propo­si­tional logic can work with are called propo­si­tions. Propo­si­tions con­sist of the prim­i­tives as well as any­thing of the form where and are propo­si­tions. Note for pedants, this de­scrip­tion al­lows the ex­is­tence of propo­si­tions that can’t be bro­ken down into a finite num­ber of prim­i­tives, we don’t want such propo­si­tions.

Let be the set of all propo­si­tions formed by tak­ing any ar­bi­trary propo­si­tions , and , in any of the fol­low­ing three ar­range­ments.




The set is the set of ax­ioms, and the three forms shown above are the in­finite ax­iom schema. For ex­am­ple, tak­ing and then ap­ply­ing the first schema gets . So this is an ax­iom.

We say that a set of propo­si­tions im­plies an­other propo­si­tion , when there ex­ists a proof of from . Write this as .

A proof of a propo­si­tion form is a list of propo­si­tions of length such that and for each , fulfills at least one of the fol­low­ing 3 con­di­tions.



3) This is called Mo­dus po­nens

Ex­am­ple Proof

For ex­am­ple, here is a proof of

Formed us­ing the sec­ond ax­iom schema.

Is then cre­ated us­ing the first ax­iom schema

Can be pro­duced by modus po­nens be­cause .

Is al­lowed by us­ing ax­iom schema 1 again.

Fol­lows by modus po­nens again be­cause .

Philo­soph­i­cally Im­por­tant Takeaways

The no­tion of math­e­mat­i­cal proof is fully for­mal­ized. There is an en­tirely me­chan­i­cal, and fairly fast, method of ver­ify­ing proofs. Proofs can be gen­er­ated in a finite amount of time, by brute force search, but this can be much slower.

The proof frame­work only be­lieves things that you have ac­tu­ally proved in it. From our point of view out­side the frame­work, the proof of also shows that , but to ac­tu­ally prove that within the frame­work, you have to go through all the steps again.