Craig DeLancey · A Concise Introduction to Logic, Ch. 2 · CC BY-SA 4.0
Propositional logic has atomic propositions (P, Q, R) and five connectives: not, and, or, implies, iff. A well-formed formula is built recursively from these pieces. Parsing a formula means finding its structure.
Atomic propositions
An atomic proposition is a statement that is either true or false, with no internal logical structure. We use capital letters P, Q, R as variables standing for any proposition.
Scheme
; Atomic propositions: just symbols; We represent them as Scheme symbols
(define P (quote P))
(define Q (quote Q))
(define R (quote R))
(display "Atomic propositions: ")
(display (list P Q R))
Connectives
The five connectives build compound formulas from simpler ones.
Symbol
Name
English
Arity
¬
Negation
not P
1 (unary)
∧
Conjunction
P and Q
2 (binary)
∨
Disjunction
P or Q
2 (binary)
→
Conditional
if P then Q
2 (binary)
↔
Biconditional
P if and only if Q
2 (binary)
Well-formed formulas
A well-formed formula (wff) is defined recursively: every atom is a wff. If A is a wff, then (not A) is a wff. If A and B are wffs, then (A and B), (A or B), (A implies B), and (A iff B) are wffs. Nothing else is a wff.
Scheme
; Formulas as S-expressions (already trees!); (not P); (and P Q); (or P Q); (implies P Q); (iff P Q); Check if something is a well-formed formula
(define (atom? x) (symbol? x))
(define (wff? f)
(cond
((atom? f) #t)
((not (list? f)) #f)
((and (= (length f) 2) (equal? (car f) (quote neg)))
(wff? (cadr f)))
((and (= (length f) 3)
(member (car f) (list (quote and) (quote or)
(quote implies) (quote iff))))
(and (wff? (cadr f)) (wff? (caddr f))))
(else#f)))
; Test
(display "(implies (and P Q) R) is wff? ")
(display (wff? (list (quote implies) (list (quote and) (quote P) (quote Q)) (quote R)))) (newline)
(display "(and P) is wff? ")
(display (wff? (list (quote and) (quote P)))) (newline)
(display "P is wff? ")
(display (wff? (quote P)))
Parsing a formula means recovering its tree structure. The main connective is the root of the parse tree: the last connective applied. For (P ∧ Q) → R, the main connective is → because implication was applied last.