**Home** / **first order logic proof calculator** / First-Order Logic

Chapter 10

First-Order Logic

10.1 Overview

First-Order Logic is the calculus one usually has in mind when using

the word ``logic''. It is expressive enough for all of mathematics,

except for those concepts that rely on a notion of construction or

computation. However, dealing with more advanced concepts is often

somewhat awkward and researchers often design specialized logics

for that reason.

Our account of first-order logic will be similar to the one of

propositional logic. We will present

? The syntax, or the formal language of first-order logic, that

is symbols, formulas, sub-formulas, formation trees, substitution,

etc.

? The semantics of first-order logic

? Proof systems for first-order logic, such as the axioms, rules,

and proof strategies of the first-order tableau method and refinement

logic

? The meta-mathematics of first-order logic, which established

the relation between the semantics and a proof system

In many ways, the account of first-order logic is a straightforward

extension of propositional logic. One must, however, be aware that

there are subtle differences.

10.2 Syntax

The syntax of first-order logic is essentially an extension of propositional

logic by quantification and . Propositional variables are replaced

by n-ary predicate symbols (P , Q, R) which may be instantiated with

either variables (x, y, z, ...) or parameters (a, b, ...). Here

is a summary of the most important concepts.

101

102 CHAPTER 10. FIRST-ORDER LOGIC

(1) Atomic formulas are expressions of the form P c1..cn where P is

an n-ary predicate symbol and the ci are variables or parameters.

Note that many accounts of first-order logic use terms built

from variables and function symbols instead of parameters. This

makes the formal details a bit more complex.

(2) Formulas are built from atomic formulas using logical connectives

and quantifiers.

Every atomic formula is a formula.

If A and B are formulas and x is a variable then (A), ?A, A B,

A B, A B, (x)A, and (x)A are formulas.

(3) Pure formulas are formulas without parameters.

(4) The degree d(A) of a formula A is the number of logical connectives

and quantifiers in A.

(5) The scope of a quantifier is the smallest formula that follows

the quantifier.

In (x)P x Qx the scope of (x) is just P x, while Qx is outside

the scope of the quantifier. To include Qx in the scope of (x)

one has to add parentheses: (x)(P x Qx).

Note that the conventions about the scope of quantifiers differ

in the literature.

(6) Free and bound variables are defined similarly to Second-Order

Propositional Logic

A variable x occurs bound in A if it occurs in the scope of a

quantifier. Any other occurrence of x in A is free.

(7) Closed formulas (or sentences) are formulas without free variables.

This is the default from now on.

(8) Substitution: A|x

a (or A[a/x]) is the result of replacing every

free occurrence of the variable x in A by the parameter a.

The technical definition is similar to the one for P 2. However,

since the term being substituted for x does not contain variables,

capture cannot occur.

(9) Subformulas are defined similar to propositional logic.

The only modification is that for any parameter a the formula

A|x

a is an immediate subformula of (x)A and (x)A.

(10) The formation tree of a formula F is a representation of all

subformulas of A in tree format.

That is, the root of the tree is F .

The sucessor of a formula of the form ?A is A.

The successors of A B, A B, A B are A and B.

10.3. SEMANTICS 103

The successors of (x)A and (x)A are A|x for all parameters ai.

ai

Note that quantifiers usually have infinitely many successors.

Atomic formulas have no successors.

10.3 Semantics

The semantics of first-order logic, like the one of propositional

logic and P 2, is based on a concept of valuations. In propositional

logic, it was sufficient to assign values to all propositional variables

and then extend the evaluation from atoms to formulas in a canonical

fashion. In P 2, the semantics of quantified formulas was defined

in terms of the values of all immediate subformulas:

v[(p)A] = (v|p )[A] B (v|p

f

t )[A].

In first-order logic, we will proceed in the same way. However,

since we don't have propositional variables anymore, we have to explain

the meaning of atomic formulas first.

The standard approach is to interpret parameters by elements of

some universe U and n-ary predicates by subsets of Un. A closed

formula P a1..an then expresses the fact that the interpretations ki U

of the ai, taken together as n-tuple (k1, .., kn), form an element of

the interpretation of P .

Smullyan's approach is similar to the above idea but avoids set

theory altogether. Instead, he introduces U-formulas, where the

elements of the universe U are used as parameters and defines first-order

valuations as canonical extensions of boolean valuations on the set

EU of all closed U-formulas. The semantics of arbitrary formulas

is then defined by a mapping from the set of parameters into U.

Creator: TeX output 2010.10.22:1915

Producer: dvipdfm 0.13.2c, Copyright © 1998, by Mark A. Wicks

CreationDate: Tue Oct 4 11:46:59 2016

ModDate: Tue Oct 4 11:49:46 2016

Tagged: no

Form: AcroForm

Pages: 13

Encrypted: no

Page size: 595 x 842 pts (A4) (rotated 0 degrees)

File size: 181550 bytes

Optimized: no

PDF version: 1.6