Abbreviating a formula by a fresh predicate symbol.

We add a list FormAbbrevations of formula abbreviations by predicate symbols, and a map Unfold to unfold abbreviations. An abbreviation is a string S staying for any closed formula A, or an atomic formula S(x,y, z,...), staying for any A in the variables x,yz,.... We define an operator SetAbbreviation[S,A], adding the abbreviation S=A, or S(x,y,z,...)=A. In order to get shorter expressions, we do not unfold abbreviations in the linear form of a formula. We also allow abbreviations for predicates.

In[136]:=

ClearAbbreviation[] := (FormAbbreviation = {}) ;

In[137]:=

SetAbbreviation[Pred_, Var_, A_] := CompoundExpression[FormAbbreviation = Append[FormAbbreviation, Pred] ; UnfoldEq[Pred, L_] := MultiSub[A, Var, L] ;] ;

In[138]:=

SetAbbreviation[S_, A_] := SetAbbreviation[HeadPredicate[S], RemoveBlanks[ArgPredicate[S]], A] ;

In[139]:=

Unfold[S_] := UnfoldEq[HeadPredicate[S], ArgPredicate[S]] ;

In[140]:=

AbbreviationQ[S_] := MemberQ[FormAbbreviation, HeadPredicate[S]] ;

In[141]:=

ClearAbbreviation[] ;

Some examples of abbreviations.

In[142]:=

SetAbbreviation["MP", Ex["x", Un["y", "f(x)≤f(y)"]]] ;

In[143]:=

Lin[Unfold["MP"]]

Out[143]=

∃x.∀y.f(x)≤f(y)

In[144]:=

FormAbbreviation

Out[144]=

{MP}

In[145]:=

SetAbbreviation["L(x,y)", Conj["x<y", "f(x)<=f(y)"]] ;

In[146]:=

? UnfoldEq

Global`UnfoldEq

UnfoldEq[MP, L$_] := MultiSub[Ex[x, Un[y, f(x)≤f(y)]], , L$]
UnfoldEq[L, L$_] := MultiSub[Conj[x<y, f(x)<=f(y)], x,y, L$]

In[147]:=

Lin[Unfold["L(h(a),k(b))"]]

Out[147]=

(h(a)<k(b)∧f(h(a))<=f(k(b)))

Created by Mathematica  (October 17, 2006)