Review

The language of Functional Logic allows us to express simple facts (as ground atoms) as well as more complex forms of information (using logical operators, variables, and quantifiers), as in the following sentence.

The Herbrand base for a logical language is the set of all ground atoms that can be formed using the vocabulary of our language. For example, the following is the Herbrand base for a language involving two object constants a and b, one unary relation constant p, and one binary relation constant q. In this case, the Herbrand base is finite. In the presence of function constants, the Herbrand base is infinite.

A Herbrand model is an arbitrary subset of the Herbrand base. The sentences included in the model are assumed to be true, and those that are excluded are assumed to be false.

A Herbrand model can be formalized equivalently as a truth assignment. Formally, a truth assignment for a propositional vocabulary is a function assigning a truth value to each element of the Herbrand base. In what follows, we use the digit 1 as a synonym for true and 0 as a synonym for false; and we refer to the value of a constant or expression under a truth assignment i by superscripting the constant or expression with i as the superscript.

Given a truth assignment for ground atoms, the semantics of our language gives us a truth assignment for all sentences in the language - not just the ground atoms but also logical sentences and quantified sentences. For example, given the truth assignment shown above, we know that the complex sentence we saw earlier must be true.

A sentence is valid if and only if it is satisfied by every truth assignment. For example, the sentence (p(a) ∨ ¬p(a)) is valid. If a truth assignment makes p(a) true, then the first disjunct is true and the disjunction as a whole true. If a truth assignment makes p(a) false, then the second disjunct is true and the disjunction as a whole is true.

A sentence is unsatisfiable if and only if it is not satisfied by any truth assignment. For example, the sentence (p(a) ∧ ¬p(a)) is unsatisfiable. No matter what truth assignment we take, the sentence is always false.

A sentence is contingent if and only if there is some truth assignment that satisfies it and some truth assignment that falsifies it. For example, the sentence (p(a) ∧ q(a,a)) is contingent. If p(a) and q((a),(a)) are both true, it is true. If p(a) and q(a,(a)) are both false, it is false.

A sentence φ is logically equivalent to a sentence ψ if and only if every truth assignment that satisfies φ satisfies ψ and every truth assignment that satisfies ψ satisfies φ. The sentence ¬(p ∨ q) is logically equivalent to the sentence (¬p ∧ ¬q). If p and q are both true, then both sentences are false. If either p is true or q is true, then the disjunction in the first sentence is true and the sentence as a whole false. Similarly, if either p is true or q is true, then one of the conjuncts in the second sentence is false and so the sentence as a whole is false. Since both sentences are satisfied by the same truth assignments, they are logically equivalent.

A sentence φ logically entails a sentence ψ (written φ ⊨ ψ) if and only if every truth assignment that satisfies φ also satisfies ψ. For example, the sentence p logically entails the sentence (p ∨ q). Since a disjunction is true whenever one of its disjuncts is true, then (p ∨ q) must be true whenever p is true. On the other hand, the sentence p does not logically entail (p ∧ q). A conjunction is true if and only if both of its conjuncts are true, and q may be false. Of course, any set of sentences containing both p and q does logically entail (p ∧ q).

A sentence φ is consistent with a sentence ψ if and only if there is a truth assignment that satisfies both φ and ψ. A sentence ψ is consistent with a set of sentences Δ if and only if there is a truth assignment that satisfies both Δ and ψ. For example, the sentence (p ∨ q) is consistent with the sentence (¬p ∨ ¬q). However, it is not consistent with (¬p ∧ ¬q).

Equivalence, entailment, and consistency can be determined by comparing truth tables. We first determine which truth assignments satisfy the two sentences and then compare. If the the set of truth assignments that satisfy the sentences are the same, the sentences are equivalent. If the set of truth assignments that satisfies the first is a subset of the set of truth assignments that satisfy the second (as in the case below), then the first sentence logically entails the second. And, if there is at least one truth assignment that satisfies both, the sentences are consistent.

    

Unfortunately, truth tables and logic grids can be very large or even infinite, rendering this approach impractical or even impossible. Fortunately, there is another way of validating these properties and relationships.

A proof of a conclusion from a set of premises is a sequence of sentences terminating in the conclusion in which each item is either (1) a premise, (2) an instance of an axiom schema, or (3) the result of applying a rule of inference to earlier items in sequence.

A proof system is sound if and only if every provable conclusion is logically entailed, i.e. if there is a proof of a sentence φ from a set of sentences Δ, then Δ logically entails φ.

A proof system is complete if and only if every logical conclusion is provable ,i.e. if Δ logically entails φ, then there is a proof of a sentence φ from Δ.

There is a proof procedure for Propositional Logic that is both sound and complete. Moreover, the question of logical entailment for Propositional Logic is decidable - there is an effective procedure that takes any premise and any conclusion as arguments and terminates in finite time with an indication of whether or not the premise logically entails the conclusion.

The same holds true for Relational Logic. There is a sound and complete proof procedure, and the question of logical entailment is decidable.

Functional Logic is more expressive than Propositional Logic and Relational Logic - it is possible to define things in Functional Logic that cannot be defined in either of the other two logics. Unfortunately, there is no sound and complete proof procedure for Functional Logic, and the question of logical entailment for Functional Logic is not decidable.