Propositional Logic

See also: informal description of propositional logic
formal description of propositional logic
and What is Logic?.

This is a very simple semi-formal specification of the version of propositional logic called PS by Hunter in [Hunter71]. I call the specification semi-formal because I am not supplying a definition of the metalanguage in which it is written.

The system is a classical propositional logic with two connectives (not and implies) presented as a "Hilbert style" axiom system in which there is just one inference rule, modus ponens, and three axiom schemata.

<formula> ::= <variable> (any single letter as a propositional variable) | <formula> (negation) | <formula> <formula> (implication)

An interpretation is a map assigning to each propositional variable one of the two truth values true and false. The truth value of a formula f under an interpretation i is val i f, where val is a (higher order) function taking two successive arguments, an interpretation i and a propositional formula f. val is defined as follows (function application is shown as juxtaposition, brackets are not necessary for simple arguments): val i ( f) = if (val i f) = true then false else true val i (f1 f2) = if (val i f1) = false then true else (val i f2)

A formula is tautological (and hence true) if it is true under every interpretation and contradictory (and hence false) if it is false under every interpretation.

There is just one inference rule, modus ponens, and three axiom schemata, as follows. Modus Ponens From two theorems, one of the form: A and the other of the form: A B where A and B are arbitrary formulae, the conclusion: B may be derived. Axiom Schemata All instances of the following three schemata are theorems: A (B A) ((A (B C)) ((A B) (A C))) (( A B) (B A))