CFOL - Classical First-Order Logic

CFOL adds quantification to CPL.

Semantics

Truth Values

Common labels for the values include:

T

1

true

F

0

false

Truth Tables

The value of a sentence with a truth-functional operator is determined by the values of its operands according to the following tables.

Negation
¬
T F
F T
Conjunction
∧ T F
T T F
F F F
Disjunction
∨ T F
T T T
F T F

Defined Operators

The Material Conditional ⊃ is definable in terms of disjunction:

A ⊃ B \(:=\) ¬A ∨ B

Likewise the Material Biconditional ≡ is defined in terms of ⊃ and ∧:

A ≡ B \(:=\) (A ⊃ B) ∧ (B ⊃ A)
Material Conditional
⊃ T F
T T F
F T T
Material Biconditional
≡ T F
T T F
F F T

Compatibility Tables

CFOL does not have separate Assertion or Conditional operators, but we include tables and rules for them, for cross-compatibility.

Assertion
⚬
T T
F F
Conditional
→ T F
T T F
F T T
Biconditional
↔ T F
T T F
F F T

Predication

The value of predicated sentences are handled in terms of a predicate's extension.

A sentence with n-ary predicate \(P\) over parameters \(\langle a_0, ... ,a_n\rangle\) has the value T iff \(\langle a_0, ... ,a_n\rangle\) is in the extension of \(P\).

Quantification

Existential

An existential sentence is true just when the sentence resulting in the subsitution of some constant in the domain for the variable is true.

Universal

A universal sentence is true just when the sentence resulting in the subsitution of each constant in the domain for the variable is true.

Consequence

Logical Consequence is defined in the standard way:

Logical Consequence

C is a Logical Consequence of A iff all models where the value of A is T are models where C also has the value T.

Tableaux

Nodes

Each node consists of a sentence.

Trunk

To build the trunk for an argument, add a node for each premise, and a node with the negation of the conclusion.

To build the trunk for the argument A1 ... An ∴ B write:
A1
⋮
An
¬B

Closure

⊗Contradiction Closure[source]
A
⋮
¬A
⊗
⊗¬=Self Identity Closure[source]
⋮
a ≠ a
⊗
⊗¬E!Non Existence Closure[source]
⋮
¬E!a
⊗

Rules

In general, rules for connectives consist of two rules per connective: a plain rule, and a negated rule. The special case of negation only one rule for double negation.

There is also a special rule for the Identity predicate.

Additional rules are given for the quantifiers.

Operator Rules

¬ Rules
¬¬KDouble Negation[source]
¬¬A
⋮
A
∧ Rules
∧KConjunction[source]
A ∧ B
⋮
A
B
¬∧KConjunction Negated[source]
¬(A ∧ B)
⋮
¬A
¬B
∨ Rules
∨KDisjunction[source]
A ∨ B
⋮
A
B
¬∨KDisjunction Negated[source]
¬(A ∨ B)
⋮
¬A
¬B
⊃ Rules
⊃KMaterial Conditional[source]
A ⊃ B
⋮
¬A
B
¬⊃KMaterial Conditional Negated[source]
¬(A ⊃ B)
⋮
A
¬B
≡ Rules
≡KMaterial Biconditional[source]
A ≡ B
⋮
¬A
¬B
B
A
¬≡KMaterial Biconditional Negated[source]
¬(A ≡ B)
⋮
A
¬B
¬A
B

Quantifier Rules

∃ Rules
∃KExistential[source]
∃xFx
⋮
Fa
¬∃KExistential Negated[source]
¬∃xFx
⋮
∀x¬Fx
∀ Rules
∀KUniversal[source]
∀xFx
⋮
Fa
¬∀KUniversal Negated[source]
¬∀xFx
⋮
∃x¬Fx

Compatibility Rules

⚬ Rules
⚬KAssertion[source]
⚬A
⋮
A
¬⚬KAssertion Negated[source]
¬⚬A
⋮
¬A
→ Rules
→KConditional[source]
A → B
⋮
¬A
B
¬→KConditional Negated[source]
¬(A → B)
⋮
A
¬B
↔ Rules
↔KBiconditional[source]
A ↔ B
⋮
¬A
¬B
B
A
¬↔KBiconditional Negated[source]
¬(A ↔ B)
⋮
A
¬B
¬A
B

Notes

References