index_16.html

Intuitionistic Logic: f function and fg injective imply g injective.
( Fun_f∧Inj_fg ⇒ Inj_g )

In this example we interpret a simple equational reasoning. Assume f is a function, and fg is injective, in order to prove that g is injective. Take any a, b, and assume g(a)=g(b), in order to prove a=b. Since f is a function, we have fg(a)=fg(b). Since fg is injective, we conclude a=b, as wished.
Below we interpret this equational reasoning as a recursive winning strategy for Eloise using intuitionistic backtracking.

There is a recursive winning strategy for Eloise. We do not describe it in full. The idea is that we read the proof itself as a strategy. Each time we invoke a particular hypothesis, or the thesis, we backtrack to it. The move by Abelard or Eloise corresponds to the logical rule we apply there.

In[395]:=

SetAbbreviation["Fun_f", Un["x", Un["y", Impl[" ... nj_g", Un["x", Un["y", Impl["g(x)=g(y)", "x=y"]]]] ;

In[398]:=

Out[398]=

Out[399]=

Dotted positions (reminder). We mark with a big dot any position to which Eloise can backtrack to: all negative judgements of the tree, and the last positive judgement of the tree.

In[400]:=

savedplay = ( "move 1" "Box" ) ; ... istic, ConstructiveImplication, CutFree", "TreeWidth=900, FontSize=12", savedplay]

[Graphics:../HTMLFiles/index_1537.gif]

[Graphics:../HTMLFiles/index_1539.gif]

$\n\n$

[Graphics:../HTMLFiles/index_1541.gif]

[Graphics:../HTMLFiles/index_1543.gif]

[Graphics:../HTMLFiles/index_1545.gif]

Goal of:

Eloise

Goal of:

Abelard

${} , ((Fun_f∧Inj_fg)Inj_g),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1556.gif]

[Graphics:../HTMLFiles/index_1558.gif]

[Graphics:../HTMLFiles/index_1560.gif]

Goal of:

Eloise

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g)} , ((Fun_f∧Inj_fg)Inj_g),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1571.gif]

[Graphics:../HTMLFiles/index_1573.gif]

[Graphics:../HTMLFiles/index_1575.gif]

Goal of:

Eloise

${} , (Fun_f∧Inj_fg),  {}$

${((Fun_f∧Inj_fg)Inj_g)}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1587.gif]

[Graphics:../HTMLFiles/index_1589.gif]

[Graphics:../HTMLFiles/index_1591.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg)}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g)} , ((Fun_f∧Inj_fg)Inj_g),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1602.gif]

[Graphics:../HTMLFiles/index_1604.gif]

[Graphics:../HTMLFiles/index_1606.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg)}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)} , Inj_g,  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1617.gif]

[Graphics:../HTMLFiles/index_1619.gif]

[Graphics:../HTMLFiles/index_1621.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg)}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g} , ∀y.(g(a)=g(y)a=y),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1632.gif]

[Graphics:../HTMLFiles/index_1634.gif]

[Graphics:../HTMLFiles/index_1636.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg)}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g(a)=g(y)a=y)} , (g(a)=g(b)a=b),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1647.gif]

[Graphics:../HTMLFiles/index_1649.gif]

[Graphics:../HTMLFiles/index_1651.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg)}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g( ... #62755;a=y), (g(a)=g(b)a=b)} , (g(a)=g(b)a=b),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1662.gif]

[Graphics:../HTMLFiles/index_1664.gif]

[Graphics:../HTMLFiles/index_1666.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg)} , g(a)=g(b),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g(a)=g(y)a=y), (g(a)=g(b)a=b), (g(a)=g(b)a=b)}$

$\n\n$

[Graphics:../HTMLFiles/index_1677.gif]

[Graphics:../HTMLFiles/index_1679.gif]

[Graphics:../HTMLFiles/index_1681.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b)} , ,  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g(a)=g(y)a=y), (g(a)=g(b)a=b), (g(a)=g(b)a=b)}$

$\n\n$

[Graphics:../HTMLFiles/index_1693.gif]

[Graphics:../HTMLFiles/index_1695.gif]

[Graphics:../HTMLFiles/index_1697.gif]

Goal of:

Eloise

${} , (Fun_f∧Inj_fg),  {g(a)=g(b), }$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1708.gif]

[Graphics:../HTMLFiles/index_1710.gif]

[Graphics:../HTMLFiles/index_1712.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), } , Fun_f,  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1723.gif]

[Graphics:../HTMLFiles/index_1725.gif]

[Graphics:../HTMLFiles/index_1727.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f} , ∀y.(g(a)=yf(g(a))=f(y)),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1738.gif]

[Graphics:../HTMLFiles/index_1740.gif]

[Graphics:../HTMLFiles/index_1742.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y))} , (g(a)=g(b)f(g(a))=f(g(b))),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1753.gif]

[Graphics:../HTMLFiles/index_1755.gif]

[Graphics:../HTMLFiles/index_1757.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... #62755;f(g(a))=f(g(b)))} , (g(a)=g(b)f(g(a))=f(g(b))),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1768.gif]

[Graphics:../HTMLFiles/index_1770.gif]

[Graphics:../HTMLFiles/index_1772.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... g(b))), (g(a)=g(b)f(g(a))=f(g(b)))} , f(g(a))=f(g(b)),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1783.gif]

[Graphics:../HTMLFiles/index_1785.gif]

[Graphics:../HTMLFiles/index_1787.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... (a)=g(b)f(g(a))=f(g(b))), f(g(a))=f(g(b))} , ,  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1799.gif]

[Graphics:../HTMLFiles/index_1801.gif]

[Graphics:../HTMLFiles/index_1803.gif]

Goal of:

Eloise

${} , (Fun_f∧Inj_fg),  {g(a)=g(b), , Fun_f, ͦ ... (g(a)=g(b)f(g(a))=f(g(b))), (g(a)=g(b)f(g(a))=f(g(b))), f(g(a))=f(g(b)), }$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1814.gif]

[Graphics:../HTMLFiles/index_1816.gif]

[Graphics:../HTMLFiles/index_1818.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... f(g(a))=f(g(b))), f(g(a))=f(g(b)), } , Inj_fg,  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1829.gif]

[Graphics:../HTMLFiles/index_1831.gif]

[Graphics:../HTMLFiles/index_1833.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... )), , Inj_fg} , ∀y.(f(g(a))=f(g(y))a=y),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1844.gif]

[Graphics:../HTMLFiles/index_1846.gif]

[Graphics:../HTMLFiles/index_1848.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... .(f(g(a))=f(g(y))a=y)} , (f(g(a))=f(g(b))a=b),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1859.gif]

[Graphics:../HTMLFiles/index_1861.gif]

[Graphics:../HTMLFiles/index_1863.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... (f(g(a))=f(g(b))a=b)} , (f(g(a))=f(g(b))a=b),  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1874.gif]

[Graphics:../HTMLFiles/index_1876.gif]

[Graphics:../HTMLFiles/index_1878.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... (a))=f(g(b))a=b), (f(g(a))=f(g(b))a=b)} , a=b,  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1889.gif]

[Graphics:../HTMLFiles/index_1891.gif]

[Graphics:../HTMLFiles/index_1893.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... ))a=b), (f(g(a))=f(g(b))a=b), a=b} , ,  {}$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g)}$

$\n\n$

[Graphics:../HTMLFiles/index_1905.gif]

[Graphics:../HTMLFiles/index_1907.gif]

[Graphics:../HTMLFiles/index_1909.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... ))=f(g(y))a=y), (f(g(a))=f(g(b))a=b), (f(g(a))=f(g(b))a=b), a=b, }$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g( ... #62755;a=y), (g(a)=g(b)a=b)} , (g(a)=g(b)a=b),  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1920.gif]

[Graphics:../HTMLFiles/index_1922.gif]

[Graphics:../HTMLFiles/index_1924.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... ))=f(g(y))a=y), (f(g(a))=f(g(b))a=b), (f(g(a))=f(g(b))a=b), a=b, }$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g( ... 5;a=y), (g(a)=g(b)a=b), (g(a)=g(b)a=b)} , a=b,  {}$

$\n\n$

[Graphics:../HTMLFiles/index_1935.gif]

[Graphics:../HTMLFiles/index_1937.gif]

[Graphics:../HTMLFiles/index_1939.gif]

Goal of:

Eloise

${(Fun_f∧Inj_fg), g(a)=g(b), , Fun_f, ∀y.(g(a)=yf(g(a))=f(y)), (g(a ... ))=f(g(y))a=y), (f(g(a))=f(g(b))a=b), (f(g(a))=f(g(b))a=b), a=b, }$

Goal of:

Abelard

${((Fun_f∧Inj_fg)Inj_g), ((Fun_f∧Inj_fg)Inj_g), Inj_g, ∀y.(g( ... (a)=g(b)a=b), (g(a)=g(b)a=b), a=b} , ,  {}$

[Graphics:../HTMLFiles/index_1949.gif]

( move 1 Box ) move 2 L ... move 21 R move 22 Atom move 23 drop

Created by Mathematica (November 11, 2006)