truth-value semantics for classical propositional logic


In classical propositional logicPlanetmathPlanetmath, an interpretationMathworldPlanetmathPlanetmath of a well-formed formula (wff) p is an assignment of truth (=1) or falsity (=0) to p. Any interpreted wff is called a proposition.

An interpretation of all wffs over the variable set V is then a Boolean function on V¯. However, one needs to be careful, for we do not want both p and ¬⁢p be interpreted as true simultaneously (at least not in classical propositional logic)! The proper way to find an interpretation on the wffs is to start from the atoms.

Call any Boolean-valued function ν on V a valuation on V. We want to extend ν to a Boolean-valued function ν¯ on V¯ of all wffs. The way this is done is similar to the construction of wffs; we build a sequence of functions, starting from ν on V0, next ν1 on V1, and so on… Finally, we take the union of all these “approximations” to arrive at ν¯. So how do we go from ν to ν1? We need to interpret ¬⁢p and p∨q from the valuations of atoms p and q. In other words, we must also interpret logical connectives too.

Before doing this, we define a truth function for each of the logical connectives:

  • •

    for ¬, define f:{0,1}→{0,1} given by f⁢(x)=1-x.

  • •

    for ∨, define g:{0,1}2→{0,1} given by g⁢(x,y)=max⁡(x,y).

As we are trying to interpret ¬ (not) and ∨ (or), the choices for f and g are clear. The values 0,1 are interpreted as the usual integers (so they can be subtracted and ordered, etc…). Hence f and g make sense.

Next, recall that Vi are sets of wffs built up from wffs in Vi-1 (see construction of well-formed formulas for more detail). We define a function νi:Vi→{0,1} for each i, as follows:

  • •

    ν0:=ν

  • •

    suppose νi has been defined, we define νi+1:Vi+1→{0,1} given by

    νi+1⁢(p):={νi⁢(p)if ⁢p∈Vi,f⁢(νi⁢(q))if ⁢p=¬⁢q⁢ for some ⁢q∈Vi,g⁢(νi⁢(q),νi⁢(r))if ⁢p=q∨r⁢ for some ⁢q,r∈Vi.

Finally, take ν¯ to be the union of all the approximations:

ν¯:=⋃i=0∞νi.

Then, by unique readability of wffs, ν¯ is an interpretation on V¯.

Remark. If ⟂ is included in the languagePlanetmathPlanetmath of the logic (as the symbol for falsity), we also require that νi⁢(⟂)=ν¯⁢(⟂)=0.

Remark V¯ can be viewed as an inductive setMathworldPlanetmath over V with respect to the ¬ and ∨, viewed as operationsMathworldPlanetmath on V¯. Furthermore, V¯ is freely generated by V, since each Vi+1 can be partitioned into sets Vi, {(p∨q)∣p,q∈Vi}, and {(¬⁢p)∣p∈Vi}, and each partition is non-empty. As a result, any valuation ν on V uniquely extends to a valuation ν¯ on V¯.

Definitions. Let p,q be wffs in V¯.

  • •

    p is true or satisfiable for some valuation ν if ν¯⁢(p)=1 (otherwise, it is false for ν).

  • •

    p is true for every valuation ν, then p is said to be valid (or tautologous). If p is false for every ν, it is invalid. If p is valid, we write ⊧p.

  • •

    p implies q for a valuation ν if ν¯⁢(p)=1 implies ν¯⁢(q)=1. p semantically implies if p implies q for every valuation ν, and is denoted by p⊧q.

  • •

    p is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to q for ν if ν¯⁢(p)=ν¯⁢(q). They are semantically equivalent if they are equivalent for every ν, and written p≡q.

Semantical equivalence is an equivalence relation on V¯.

The above can be easily generalized to sets of wffs. Let T be a set of propositions.

  • •

    T is true or satisfiable for ν if ν¯⁢(T)={1} (otherwise, it is false for ν).

  • •

    T is valid if it is true for every ν; it is invalid if it is false for every ν. If T is valid, we write ⊧T.

  • •

    T implies p for ν if ν¯⁢(T)={1} implies ν¯⁢(p)=1. T semantically implies p if T implies p for every ν, and is denoted by T⊧p.

  • •

    T1 implies T2 for ν if, for every p∈T2, T1 implies p for ν. T1 semantically implies T2 if T1 implies T2 for every ν, and is denoted by T1⊧T2.

  • •

    T1 is equivalent to T2 for ν if for some valuation ν, T1 implies T2 for ν and T2 implies T1 for ν. T1 and T2 are semantically equivalent if T1⊧T2 and T2⊧T1, written T1≡T2.

Clearly, ⊧p iff ∅⊧p, and T⊧p iff T⊧{p}.

Title truth-value semantics for classical propositional logic
Canonical name TruthvalueSemanticsForClassicalPropositionalLogic
Date of creation 2013-03-22 18:51:20
Last modified on 2013-03-22 18:51:20
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 20
Author CWoo (3771)
Entry type Definition
Classification msc 03B05
Synonym entail
Defines truth-value semantics
Defines valuation
Defines interpretation
Defines valid
Defines invalid
Defines satisfiable