# Chains of equivalences

This document gives a short description of how Carnap presents the systems of "chains of equivalences" that allow transformations of sentences into equivalent sentences, e.g., in disjunctive or conjunctive normal form.

## Notation

The system uses the parser/syntax of forall x: Calgary and the Open Logic Text.

The different admissible keyboard abbreviations for the different connectives are as follows:

Connective Keyboard
`->`, `=>`, `>`
`/\`, `&`, `and`
`\/`, `|`, `or`
↔︎ `<->`, `<=>`
¬ `-`, `~`, `not`
`!?`, `_|_`
`A`, `@`
`E`, `3`

Proofs consist of a series of lines. Every line contains a formula followed by a `:` and then a rule abbreviation. The first line is justified by `:PR`. The available rules are all equivalences, and can be applied to subformulas of a given formula. It is assumed that every line follows from the immediately preceding line by one of the equivalence rules below.

## Equivalences for TFL (propositional logic)

The equivalence proof checker is selected using `.ZachPropEq`.

Ex1
A \/ ~(B \/ C) :PR A \/ ~(C \/ B) :Comm A \/ (~C /\ ~B) :DeM (A \/ ~C) /\ (A \/ ~B) :Dist

The following exchange rules are allowed. They can be used within a propositional context Φ, and in both directions. In other words, any formula occurrence on the left of the table below can be replaced by the corresponding formula on the right, and vice versa.

Rule Abbreviation Premises Conclusion
Double Negation `DN` ¬¬φ φ
Conditional `Cond` (φψ) φψ)
φψ) (φψ)
Biconditional Exchange `Bicond` (φ↔︎ψ) ((φψ)∧(ψφ))
DeMorgan's Laws `DeM` ¬(φψ) φ∨¬ψ)
¬(φψ) φ∧¬ψ)
Commutativity `Comm` (φψ) (ψφ)
(φψ) (ψφ)
Associativity `Assoc` (φ∧(ψχ)) ((φψ)∧χ)
(φ∨(ψχ)) ((φψ)∨χ)
Distributivity `Dist` (φ∨(ψχ)) ((φψ)∧(φχ))
(φ∧(ψχ)) ((φψ)∨(φχ))
((φψ)∨(φχ)) (φ∧(ψχ))
Idempotence `Id` (φφ) φ
(φφ) φ
Absorption `Abs` (φ∧(φψ)) φ
(φ∨(φψ)) φ
Simplification `Simp` (φ∧(ψ∨¬ψ)) φ
(φ∨(ψ∧¬ψ)) φ
(φ∨(ψ∨¬ψ)) (ψ∨¬ψ)
(φ∧(ψ∧¬ψ)) (ψ∧¬ψ)

The rules for distributivity, absorption, and simplification allow for implicit commutativity, so e.g., `Distr` also allows replacing (ψχ) ∨ φ by (ψφ) ∧ (χφ), and `Simp` allows replacing ψψ) ∧ φ by φ.

If the conclusion of the target entailment is left empty, and the `tests` option is set, the checker will accept any proof where the last line meets the test. So for instance, to require students to transform a sentence into conjunctive normal form, you would assign

`````````{.ProofChecker .ZachPropEq tests="CNF"}
Ex1 A \/ ~(B \/ C) :|-:
|A \/ ~(B \/ C) :PR
`````````
Ex1
A \/ ~(B \/ C) :PR

A proof playground is also supported.

`````````{.Playground .ZachPropEq}
`````````
Playground

The available tests are the same as for translation exercises, and can be combined. If combined, multiple tests have to be separated by spaces. Tests also work on playgrounds.

Name Effect
`CNF` Requires conjunctive normal form
`DNF` Requires disjunctive normal form
`maxCon:N` Requires that the translation contain N or fewer connectives
`maxNot:N` Requires that the translation contain N or fewer negations
`maxAnd:N` Requires that the translation contain N or fewer conjunctions
`maxIff:N` Requires that the translation contain N or fewer biconditionals
`maxIf:N` Requires that the translation contain N or fewer conditionals
`maxOr:N` Requires that the translation contain N or fewer disjunctions
`maxFalse:N` Requires that the translation contain N or fewer falsity constants
`maxAtom:N` Requires that the translation contain N or fewer atomic sentences

## The FOL Systems

The system `.ZachFOLEq` extends the rules of `.ZachPropEq` by equivalence rules for quantifiers, also applied in arbitrary contexts Φ, and in either direction. Those are:

Rule Abbreviation Premises Conclusion
Variable Renaming `VR` xφ(x) yφ(y)
xφ(x) yφ(y)
Quantifier Exchange `QX` xyφ(x,y) yxφ(y)
xyφ(x,y) yxφ(x,y)
Quantifier Negation `QN` ¬∀xφ(x) x¬φ(x)
¬∃xφ(x) x¬φ(x)
Quantifier Distribution `QD` x(φ(x)∧ψ(x)) xφ(x) ∧ ∀xψ(x)
x(φ(x)∨ψ(x)) xφ(x) ∨ ∃xψ(x)
Quantifier Shift for `QSA` x(φ(x)∧ψ) xφ(x) ∧ ψ
x(φ(x)∨ψ) xφ(x) ∨ ψ
x(φ(x)→ψ) xφ(x) → ψ
x(ψφ(x)) ψ → ∀xφ(x)
Quantifier Shifts for `QSE` x(φ(x)∧ψ) xφ(x) ∧ ψ
x(φ(x)∨ψ) xφ(x) ∨ ψ
x(φ(x)→ψ) xφ(x) → ψ
x(ψφ(x)) ψ → ∃xφ(x)

Note that Carnap actually considers all formulas equal up to renaming of bound variables. Thus, the `VR` rules are provided just for completeness (and will allow any number of renamings of bound variables). Any variable renaming necessary to apply a quantifier shift can be done implicitly without first invoking the `VR` rule.

Testing of correctness can become quite slow, so it is recommended to not do this on every button press and use `feedback="manual"` instead.

The FOL system has an additional test, `PNF`, that requires the final line to be in prenex normal form.

`````````{.ProofChecker .ZachFOLEq options="resize" feedback="manual" tests="PNF"}
Ex2 ~(Ax P(x) <-> Ey Q(y)) :|-:
|~(Ax P(x) <-> Ey Q(y)) :PR
`````````
Ex2
~(Ax P(x) <-> Ey Q(y)) :PR ~((Ax P(x) -> Ey Q(y)) /\ (Ey Q(y) -> Ax P(x))) :Bicond ~(Ax P(x) -> Ey Q(y)) \/ ~(Ey Q(y) -> Ax P(x)) :DeM ~(Ax P(x) -> Ey Q(y)) \/ ~Ay( Q(y) -> Ax P(x)) :QSA ~(Ax P(x) -> Ey Q(y)) \/ ~AyAx( Q(y) -> P(x)) :QSA ~(Ax P(x) -> Ey Q(y)) \/ Ey~Ax( Q(y) -> P(x)) :QN ~(Ax P(x) -> Ey Q(y)) \/ EyEx~( Q(y) -> P(x)) :QN (Ax P(x) /\ ~Ey Q(y)) \/ EyEx~( Q(y) -> P(x)) :Cond (Ax P(x) /\ Ay~ Q(y)) \/ EyEx~( Q(y) -> P(x)) :QN (Ax P(x) /\ Ax~ Q(x)) \/ EyEx~( Q(y) -> P(x)) :VR Ax(P(x) /\ ~Q(x)) \/ EyEx~( Q(y) -> P(x)) :QD Ey[Ax(P(x) /\ ~Q(x)) \/ Ex~( Q(y) -> P(x))] :QSE EyEx[Ax(P(x) /\ ~Q(x)) \/ ~( Q(y) -> P(x))] :QSE