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 ... AnB 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