Sign of a formula

We can add to any formula a positive or negative sign in front. If A is any formula, we denote the positive version of A by t.A (to be read: "A is true") and the negative version of A by f.A (to be read: "A is false"). We call t.A, f.A a judgment (about the truth or the falsity of A). For most uses, we can identify t.A with A, and f.A with ¬A, but in some case the use of judgments is essential.

In[46]:=

PosSign = "." ; NegSign = "." ;

We define an operation, Dual[.], switching positive and negative sign.

In[47]:=

Dual[s_] := If[sPosSign, NegSign, PosSign] ;

Each sign corresponds to a player. t. corresponds to Eloise, and f. corresponds to Abelard. We define two maps, sending the sign into the corresponding player, and the player into the corresponding sign.

In[48]:=

SignToPlayer[s_] := If[sPosSign, "Eloise", "Abelard"] ;

In[49]:=

PlayerToSign[p_] := If[p == "Eloise", PosSign, NegSign] ;

We extend Linearization operator to deal with judgments. Lin[A,s] linearizes the formula A, then adds the sign s in front of it.

In[50]:=

Lin[A_, s_]          := StringJoin[s, Lin[A]] ;

An example of judgment: the formula t.F4, or "F4 is true".

In[51]:=

Lin[F4, PosSign]

Out[51]=

.(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

Created by Mathematica  (October 17, 2006)