Intuitionistic Existential Graphs from a non traditional point of view

TL;DR

This paper introduces a new version of intuitionistic existential graphs, combining recursive rules and geometric representations to improve deduction management and better connect topology with propositional logic.

Contribution

It develops an enhanced intuitionistic existential graph system with recursive rules and geometric symbols, improving deduction handling and logical-topological representation.

Findings

Equivalent to the intuitionistic propositional calculus

Incorporates second-degree deductive rules for better deduction management

Uses geometric symbols to relate topology with propositional logic

Abstract

In this article we develop a new version of the intuitionist existential graphs presented by Arnol Oostra [4]. The deductive rules presented in this article have the same meaning as those described in the work of Yuri Poveda [5], because the deductions according to the parity of the cuts are eliminated and are replaced by a finite set of recursive rules. This way, $ Alfa_I $ the existential graphs system for intuitional propositional logic follows the course of the deductive rules of the system $ Alfa_0 $ described by Poveda [5], and is equivalent to the intuitionistic propositional calculus. In this representation the $ Alfa_0 $ system is improved, there are a series of deductive rules of second degree incorporated that previously had not been considered and that allow a better management of deductions and finally from the ideas proposed by Van Dalen [6], a mixture is incorporated in the deduction techniques, the natural deductions of the Gentzen system are combined with new system rules $ Alfa_0 $ and $ Alfa_I $. The symbols proposed for the $Alfa_I$ representation relate open, closed and quasi-open sets of the usual topology of the plot with the intuitional propositional logic, usefull for approaching new problems in the representation of this logic from a more geometrical perspective.

Equations

$$R_3:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptAB\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

$$R_7:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptAB\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-3.41666ptB\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

$$R_2:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptAB\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

$${\wedge }_i:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}8.53578pt\text{raise}-3.41666ptA\text{raise}8.53578pt\text{raise}-3.41666ptB\text{raise}-8.53578pt\text{raise}-3.41666ptA\wedge B$$

$${\perp }_e:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}8.53578pt\text{raise}-3.47223pt\perp \text{raise}-8.53578pt\text{raise}-3.41666ptA$$

$${\to }_i:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}8.53578pt\text{raise}-3.41666ptB\text{raise}-8.53578pt\text{raise}-3.57222ptA\to B\text{raise}34.14313pt\text{raise}-3.41666ptA\text{framed@@}0.0pt[A]$$

$$I_{\vee }\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptA\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-24.5pt\text{vbox}\text{vskip}18.0ptto40.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}18.0pt\text{raise}0.0pt\text{raise}-3.41666ptB\text{raise}0.0pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

$$R_2:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptAB\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

$$M{P}_i:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}-5.69052pt\text{raise}-3.41666ptB\text{raise}-5.69052pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}-5.69052pt\text{raise}-3.41666ptA\text{raise}17.07156pt\text{raise}-3.41666ptA\text{raise}-5.69052pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.47223pt⊢\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-3.41666ptB$$

$$I_{p3}:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-24.5pt\text{vbox}\text{vskip}18.0ptto40.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}18.0pt\text{raise}0.0pt\text{raise}-3.41666ptB\text{raise}0.0pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}-24.5pt\text{vbox}\text{vskip}18.0ptto40.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}18.0pt\text{raise}0.0pt\text{raise}-3.41666ptB\text{raise}0.0pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

$$E_p:\text{lx@xy@svg}\text{raise}0.0pt\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-3.41666ptB\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{framed@@}0.0pt\text{raise}0.0pt\text{raise}0.0pt\text{cirbuild@}\text{raise}0.0pt\text{raise}-3.41666ptA\text{raise}0.0pt\text{raise}-3.41666ptB\text{raise}0.0pt\text{raise}-15.5pt\text{vbox}\text{vskip}7.0ptto14.0pt\text{hfill}\text{lx@xy@buildcircle@}\text{hfill}\text{vskip}7.0pt\text{raise}0.0pt\text{raise}-3.47223pt⊢$$

Full text

Intuitionistic Existential Graphs from a non traditional point of view.

Yuri A. Poveda

  

Steven Zuluaga

Abstract. In this article we develop a new version of the intuitionist existential graphs presented by Arnol Oostra [3]. The deductive rules presented in this article have the same meaning as those described in the work of Yuri Poveda [4], because the deductions according to the parity of the cuts are eliminated and are replaced by a finite set of recursive rules. This way, $Alfa_{I}$ the existential graphs system for intuitional propositional logic follows the course of the deductive rules of the system $Alfa_{0}$ described by Poveda [4], and is equivalent to the intuitionistic propositional calculus.

In this representation the $Alfa_{0}$ system is improved, there are a series of deductive rules of second degree incorporated that previously had not been considered and that allow a better management of deductions and finally from the ideas proposed by Van Dalen [5], a mixture is incorporated in the deduction techniques, the natural deductions of the Gentzen system are combined with new system rules $Alfa_{0}$ and $Alfa_{I}$.

The symbols proposed for the $Alfa_{I}$ representation relate open, closed and quasi-open sets of the usual topology of the plot with the intuitional propositional logic, usefull for approaching new problems in the representation of this logic from a more geometrical perspective.

Keywords: Propositional calculus, intuitionism, existential graphs, deductive rules.

1 Introduction.

The following assignment is an addition to the studies made on Peirce’s existential graphs in Colombia, motivated by professor Yuri Alexander Poveda’s suggestion of finding a system of existential graphs equivalent to the intuitionistic propositional calculus. Problem to which a solution is given in this article.

Peirce’s existential graphs are deductive systems that formalize the classic logic of propositions ($alfa$ system), of predicates ($beta$ system) and the modal ($gama$ system). Likewise, these are innovative systems that contribute a totally new vision of the logic principles, which facilitate learning, management, discovery, and truth deductions, besides offering other advantages. Unfortunately, these haven’t had a great reception by the logical community; however, Roberts and Zeman have studied Peirce’s graphs in their doctorate thesis (where they precisely study the $alfa$, $beta$ and $gama$ systems); later on, Burch, Brady and Trimble; and finally in Colombia, Oostra [3], Zalamea [6] and Poveda [4].

The biggest interest of this article is first, to present the intuitionistic system of existential graphs ($GEI$) obtained from the graphic systems $ALFAo$, proposed by Yuri A. Poveda [4] and the natural deductive system for intuitionism presented by Van Dalen [5]. Secondly, to show that it is equivalent to the Intuitionistic Propositional Calculus.

In the first section the $ALFAo$ system is presented with some modifications, where the introduction of a new rule that marks the difference between $alfa$ and $ALFAo$, and a new notation that facilitates making deductions in $ALFAo$, stand out. Likewise, the calculus of rules is formalized through four definitions that are introduced at the beginning of the chapter, the symmetries of the $ALFAo$ rules are studied, and the relations of these with the Modus Ponendo Ponens, and with the insertion and elimination of the double cut. In the second section the following things are done: a presentation of the natural deduction system for intuition, extracted from the Van Dalen [5] article; the definition of two new graphs used to design the implication and the disjunction of a new system, as well as a function used to translate graphs into formulas; the presentation of a system of $GEI$ ($ALFA_{I}$), who’s deductive rules are obtained from the natural deduction system presented before; the change of some of $ALFA_{I}$ basic rules for other ones (theorems of the same); and the presentation of the $ALFA_{Io}$ graphs system that is equivalent to $ALFA_{I}$. Finally, a new not-intuitionistic rule is added to the $ALFA_{Io}$ system and the equivalence of this with $ALFAo$ is studied. In the third chpater: We approach exegetically the article of Arnold Oostra in which he exposes a $GEI$ system [3] that, different to the $ALFA_{Io}$, harmonizes with $alfa$ conserving the same structure to enunciate the graphical transformation rules and the notation to present the demonstrations, and some differences between $ALFA_{Io}$ and the system proposed by Arnold Oostra are shown.

2 $ALFAo$ deductive system

$ALFAo$ is a deductive system of graphs equivalent to the Classic Propositional Calculus, defined from the existential graphs system, $alfa$ by Charles Sander Peirce. Next we will present $ALFAo$ with some modifications that attend to a simpler presentation of the same, to see a more detailed presentation of this system, refer to [3].

Primitive systems:

The rectangle , the closed curve , the letters $p_{i}$,$q_{i}$,$r_{i}$;$A_{i}$,$B_{i}$,$C_{i}$, $i\in\mathbb{N}$ and the letter $\lambda$.

The following definition formalizes in a general way the types of rules that may take place in the system. In other systems like in [3] and [6], the definition of what a deductive rule limited to first degree rules is, appears indirectly.

Deductive rules (rds):

Given $G_{1}$ y $G_{2}$ wdgs then G_{1}$$\vdash$$G_{2} is a first degree rd. 2. 2.

Given $R_{1}$,$R_{2}$,…,$R_{j}$,$R$ first degree rds then \textstyle{R_{1},R_{2},...,R_{j}}$$\textstyle{R} is a second degree rd.

System’s axiom:

System’s deductive rules:

The following rules are presented according to the deductive rule definition given previously, either of insertion or elimination. This classification appears indirectly in [4].

A) First degree deductive rules:

Of insertion: A rule is of insertion if to pass from a graphic to another letters or closed curves called cuts are drawn.

[TABLE]

Of elimination: A rule is of elimination if to pass from a graphic to another letters or cuts are eliminated.

[TABLE]

B) Second degree deductive rule:

[TABLE]

2.1 Deduction in $ALFAo$

Definition 1**.**

$G\underset{ALFAo}{\vdash}G^{{}^{\prime}}$* if and only if exists $G_{i}\vdash G_{i+1}$ rds of $ALFAo$ with $1\leq i\leq n$ where $G=G_{1}$ y $G^{{}^{\prime}}=G_{n+1}$ ($G^{{}^{\prime}}$ is formal theorem if $G$ is the axiom or a formal theorem).*

Definition 2**.**

*Given the link $\{G_{i}\underset{ALFAo}{\vdash}G_{i+1}\}_{1\leq i\leq n}$ of rds then

\textstyle{\{G_{i}\underset{ALFAo}{\vdash}G_{i+1}\}_{1\leq i\leq n}}$$\textstyle{G_{1}\vdash G_{n+1}} is a second degree rd of $ALFAo$.*

Definition 3**.**

Given \textstyle{\{R_{i}\}_{1\leq i\leq n}}$$\textstyle{R} and $\{R_{i}\}_{1\leq i\leq n}$ rds of $ALFAo$ then $R$ is a $ALFAo$ rd.

Note: It can happen that \textstyle{\{R_{i}\}_{1\leq i\leq n}}$$\textstyle{R} be a $ALFAo$ rd and that the rds $\{R_{i}\}_{1\leq i\leq n}$ and $R$ not be of $ALFAo$. [see $R_{8}$].

Definition 4**.**

Given $\{R_{i}^{{}^{\prime}}\}_{1\leq i\leq n}\notin ALFAo$ y $\{R_{j}\}_{1\leq j\leq m}\in ALFAo$ we have that

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 21.33955pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-21.20059pt\raise 8.53578pt\hbox{\hbox{\kern 3.0pt\raise-3.73483pt\hbox{\textstyle{{R_{i}^{{}^{\prime}}}{1\leq i\leq n}}}}}}}{\hbox{\kern-6.83507pt\raise-8.53578pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{R}}}}}}}}}}\Leftrightarrow\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 42.67912pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-42.26524pt\raise 8.53578pt\hbox{\hbox{\kern 3.0pt\raise-3.5711pt\hbox{\textstyle{{R{i}^{{}^{\prime}}}{1\leq i\leq n},{R{j}}_{1\leq j\leq m}}}}}}}{\hbox{\kern-6.83507pt\raise-8.53578pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{R}}}}}}}}}}**

The following rule, that translated to the Hilbert type systems correspond with the rule $\alpha\rightarrow\beta,\alpha\rightarrow\gamma\vdash\alpha\rightarrow\beta\wedge\gamma$, is used in the other existential graphic systems [3], [6], [5] in an intuituve and informal way. However here we introduce a rule of the system that isn’t deductible from this one.

\textstyle{R_{0}:}$$\textstyle{B}$$\textstyle{A}$$\textstyle{\vdash},\textstyle{A}$$\textstyle{C}$$\textstyle{\vdash}$$\textstyle{A}$$\textstyle{BC}$$\textstyle{\vdash}

Introducing this rule in $ALFAo$ as rd of the system makes it possible to, with great ease, make the deduction of the rule $\alpha,\beta\vdash\alpha\wedge\beta$ known in the Hilbert type systems as insertion of $\wedge$.

Theorem 5**.**

\textstyle{R_{0}}$$\textstyle{A}$$\textstyle{\vdash}$$\textstyle{B}$$\textstyle{\vdash}$$\textstyle{AB}$$\textstyle{\vdash},

The rule $R_{1}$ is deduced from $ALFAo$ therefore is a theorem of the system and can be suppressed as it’s basic rule.

Theorem 6**.**

R_{1}:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.95842pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 20.79785pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{AA}}}}}}{\hbox{\kern 11.016pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFAo**

[TABLE]

Note that by the definition 4 $R_{1}\in ALFAo$.

Each of the basic rules of the $ALFAo$ system (of $R_{1}$ to $R_{8}$), seem to be necessary to form an equivalent system to $CPC$, this is because originally each and every one of these were defined based on the rules of Peirce’s $alfa$ system. Nevertheless, the rules $R_{7}$ and $R_{4}$ can be supressed as the system’s basic deductive rules, since they are theorems of $ALFAo$.

Theorem 7**.**

$R_{7}$* is deductible by $R_{5}$,$R_{2}$ and $R_{8}$.*

[TABLE]

Theorem 8**.**

$R_{4}$* is deductible by $R_{5}$,$R_{2}$,$R_{6}$ and $R_{8}$.*

Theorem 9**.**

R_{8}^{-}:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 18.49445pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 40.90521pt\raise 36.98839pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 39.9034pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 52.81923pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{C}}}}}}{\hbox{\kern 52.25047pt\raise 36.98839pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 25.24231pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-10.79341pt\raise-36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{AB}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 49.97397pt\raise-36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{C}}}}}}{\hbox{\kern 25.24231pt\raise-36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFAo**

[TABLE]

It is immediately noted that the strongest rules in $ALFAo$ are $R_{8}$ and $R_{0}$, without being coincidence that they are of second degree. Similarly, it is awaited that $R_{8}^{-}$ would be equally strong to it’s inverse. This results to be true, which will be shown in the deductions of the inverse rules that remain.

Proposition 10**.**

$R_{1}^{-},R_{4}^{-},R_{5}^{-},R_{6}^{-}yR_{7}^{-}\in ALAFAo$**

2.2 $MP$ and the elimination of the double cut

The Modus Ponendo Ponens is a theorem of $ALFAo$

Theorem 11**.**

The Modus Ponendo Ponens MP:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 18.49432pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-1.35287pt\raise-5.69052pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-1.30948pt\raise-5.69052pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-15.28578pt\raise-5.69052pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-6.75pt\raise 17.07156pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-16.0pt\raise-5.69052pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 22.39705pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 47.01656pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}}}}}\in ALFAo

[TABLE]

The result presented below suggests a question: Can the Modus ponendo ponens, which is an intuitionist rule, deduce a non-intuitionist rule? The answer is clear, no. However, in $ALFAo$ the Modus Ponendo Ponens with the help of other rules, deduce the elimination of the double cut. For this reason, it is not possible to obtain an intuitionistic system of graphs from $ALFAo$, unless the vertex that unites these two rules is undone.

Theorem 12**.**

$MP$* deduces $R_{6}$.*

\textstyle{B}$$\textstyle{\underset{MP}{\vdash}}$$\textstyle{B}

It is easy to see that with $R_{2}$,$R_{0}$ and $MP$ we can deduce $R_{6}.$

From the above, it can be stated that in $ALFAo$ the implication (and disjunction) is not independent of the negation and conjunction, like it does happen in the intuitionist propositional calculus ($IPC$). Relation that must be avoided to define the intuitionist system of graphs.

3 Intuitionist Existential Graphs and the $IPC$

The first presentation of a formal system for the intuitionist logic was published by Arend Heyting in 1930 and its formalization was presented in Hilbert style (two rules of inference and a large number of axioms). Four years later, Gerhard Gentzen announced two different alternatives to formalize it: the sequencing calculus and the natural deduction, the last characterized both by having rules of insertion And elimination for each connective, as by having an abbreviated notation for the deductions. Subsequently, Arnold Oostra presented an existential graphical version, equivalent to the $IPC$, symmetric in the original sense (the one adopted in the presentations for the $alpha$ system).

This chapter shows a $GEI$ system constructed from the natural deduction system for intuitionism presented by Dirk Van Dalen [5], which preserves some of the characteristics that differentiate the $ALFAo$ system from the $alpha$ system.

The path chosen to find this system was totally different from that followed by Arnold Oostra, who was based primarily on the $alpha$ system and the Peircean legacy. For example, two new graphs were introduced, one to represent the implication and the other to represent the disjunction; However, with regard to denial and conjoint, $ALFAo$ graphs were used; In the case of the set of the basic deductive rules, we copied those of the natural deduction system for the aforementioned intuitionism, through a function that allows to make translations of formulas to graphs; And, finally, the graphical system obtained was refined.

3.1 Intuitionist Existential Graphs

Drawings that represent the implication and the disjunction:

for the implication for the disjunction.

Note: the dotted curve was used by Peirce for the modal logic as a representation of the possible; However, here this drawing is taken with a totally different connotation that will be made known later.

3.1.1 Natural Deduction for the intuitionism [5].

Primitive symbols:

The conjunction $\wedge$, the disjunction $\vee$, the implication $\rightarrow$, the parenthesis $($,$)$, the constants: false $\bot$ and true $\top$, and the letters $p_{i}$,$q_{i}$,$r_{i}$;$A_{i}$,$B_{i}$,$C_{i}$, $i\in\mathbb{N}$.

Definition 13**.**

well formed formulas ($fbf$):

An atomic proposition $p$ is a $fbf$. 2. 2.

The constants are $fbf$. 3. 3.

*If $A$ and $B$ are *$fbf$*s, then $A\wedge B$, $A\vee B$, $A\rightarrow B$ are *$fbf$s. 4. 4.

*The formulas constructed according to 1. 2. y 3. are also *$fbf$s.

Definition 14**.**

$\neg$A=A\rightarrow$$\bot

System’s deductive rules

A) First degree deductive rules

Of insertion

[TABLE]

Of elimination

[TABLE]

B) Second degree deductive rules

[TABLE]

The formulas between brakets represent canceled premises in the new deduction.

The rule $\rightarrow_{i}$ is a weak version of the Meta-theorem of the deduction that can be stated as follows: if $\alpha\vdash\beta$ then $\vdash\alpha\rightarrow\beta$. In the same way, the rule $\vee_{e}$ can be stated as follows: if $\alpha\vdash\gamma,\beta\vdash\gamma$ then $\alpha\vee\beta\vdash\gamma$.

Definition 15**.**

function of translation () of graphs to formulas.*

For every proposition $p$ and for every graphic $A$ and $B$

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.95842pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 8.7263pt\raise 17.07156pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{*}}}}}}}}}}\Longrightarrow\top** 2. 2.

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 9.95842pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-5.51563pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-1.18056pt\hbox{\textstyle{p}}}}}}{\hbox{\kern 8.7263pt\raise 17.07156pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{*}}}}}}}}}}\Longrightarrow p** 3. 3.

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-10.79341pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{AB}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\Longrightarrow\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\wedge\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-7.0434pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{*}}}}}}}}}}** 4. 4.

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-7.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\Longrightarrow\neg\quad\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}** 5. 5.

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-20.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern 1.49239pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 1.53578pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-15.28578pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\Longrightarrow\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\rightarrow\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-7.0434pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{*}}}}}}}}}}** 6. 6.

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-20.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern 1.49239pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 1.53578pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern 1.53578pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-15.28578pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-15.53578pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-15.53578pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\Longrightarrow\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{}}}}}}}}}}\vee\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 22.76228pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-7.0434pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 22.9526pt\raise 34.14313pt\hbox{\hbox{\kern 3.0pt\raise-2.3264pt\hbox{\textstyle{*}}}}}}}}}}**

3.1.2 $ALFA_{I}$ System

Then, in order to define the $ALFA_{I}$ system, the rules of the natural deduction system for intuitionism are copied by using the function defined above (as we noted at the beginning of the section), in the same manner the primitive $ALFAo$ symbols are added, it’s unique axiom, and the $R_{0}$ rule.

Primitive symbols:

The system’s symbols $ALFAo$ and the cuts and

Definition 16**.**

Well done graphs (wdg):**

The graphs constructed by the rule of construction of the $ALFAo$ system’s graphs are wdgs. 2. 2.

*If * $\textstyle{A}$

• , * $\textstyle{B}$
• are wdgs * $\textstyle{B}$

$\textstyle{A}$

• , * $\textstyle{B}$

$\textstyle{A}$

• are wdgs.*

The graphs constructed according to 1. y 2. are wdgs.

System’s axiom

System’s deductive rules

A) First degree deductive rules:

Of insertion

[TABLE]

Of elimination (the rule $E_{\bot}$ can also be considered of insertion)

[TABLE]

B) Second degree deductive rules:

[TABLE]

[TABLE]

Note: The translation of the $\rightarrow_{i}$ rule results in a weaker rule than $R_{8i}$. It was decided to take $R_{8i}$ instead of it’s weaker similar, to achieve some homogeneity or similarity with $ALFAo$. However, in the appendix, the $R_{8i}$ was tested using the rule that translates directly from $\rightarrow_{i}$, named as $R_{8id}$.

3.1.3 Deductions in $ALFA_{I}$

Theorem 17**.**

R_{8i}^{-}:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 18.49445pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 40.90521pt\raise 36.98839pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 39.9034pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 52.81923pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{C}}}}}}{\hbox{\kern 52.25047pt\raise 36.98839pt\hbox{\hbox{\kern 0.0pt\raise-15.75pt\hbox{\hbox{\vbox{\vskip 7.5pt\hbox to15.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.5pt}}}}}}}{\hbox{\kern 25.24231pt\raise 36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-10.79341pt\raise-36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{AB}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 49.97397pt\raise-36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{C}}}}}}{\hbox{\kern 25.24231pt\raise-36.98839pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFA_{I}.

The proof of this rule is similar to clasic proof.

Theorem 18**.**

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 42.67905pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.93124pt\raise 22.76208pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{C}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-38.34126pt\raise 22.76208pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-25.50578pt\raise 22.76208pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\underset{R}{\vdash}}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise-17.07156pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-6.93124pt\raise-28.4526pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{C}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-38.04787pt\raise-17.07156pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-38.34126pt\raise-28.4526pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-20.28186pt\raise-22.76208pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFA_{I}**

\textstyle{B}$$\textstyle{A}$$\textstyle{B}$$\textstyle{\underset{R_{2}}{\vdash}}$$\textstyle{\underset{R}{\vdash}}$$\textstyle{C}$$\textstyle{A}$$\textstyle{A}$$\textstyle{B}$$\textstyle{\underset{R_{2}}{\vdash}}$$\textstyle{R_{0}}$$\textstyle{A}$$\textstyle{C}$$\textstyle{A}$$\textstyle{B}$$\textstyle{\vdash},

The rule just demonstrated is a direct consequence of the use of $R_{0}$. In other systems such as $alfa$ and the $GEI$ presented by Arnold Oostra, this rule is assumed in meta-language. Henceforth, the use of it will not be sought in order to simplify the presentation of the demonstrations.

Theorem 19**.**

I_{p2}:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 85.35802pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-20.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-18.42444pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-1.05948pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-1.30948pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-4.30948pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-17.0pt\hbox{\hbox{\vbox{\vskip 10.0pt\hbox to20.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 10.0pt}}}}}}}{\hbox{\kern-37.35342pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-82.59573pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-81.02017pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-63.65521pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}}}}}\in ALFA_{I}**

\textstyle{B}$$\textstyle{A}

\textstyle{\vdash}$$\textstyle{B}$$\textstyle{A}$$\textstyle{R_{8i}}$$\textstyle{A}$$\textstyle{\underset{E_{\neg}}{\vdash}}$$\textstyle{A}

\textstyle{R_{8i}}$$\textstyle{B}$$\textstyle{A}$$\textstyle{\vdash}$$\textstyle{B}$$\textstyle{\underset{MP_{i}}{\vdash}}$$\textstyle{B}$$\textstyle{A}

\textstyle{B}$$\textstyle{A}$$\textstyle{B}$$\textstyle{A}$$\textstyle{\underset{I_{\neg}}{\vdash}}$$\textstyle{B}$$\textstyle{A}

Theorem 20**.**

E_{p}:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 91.04854pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-18.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-15.28578pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-1.35287pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-1.30948pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-86.28625pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-83.57204pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-69.63913pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-69.59573pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-45.8892pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFA_{I}**

\textstyle{A}$$\textstyle{B}$$\textstyle{\underset{E_{\neg}}{\vdash}}$$\textstyle{A}$$\textstyle{B}

\textstyle{R_{8i}}$$\textstyle{A}$$\textstyle{B}

\textstyle{\vdash}$$\textstyle{\underset{MP_{i}}{\vdash}}$$\textstyle{B}$$\textstyle{B}$$\textstyle{A}$$\textstyle{B}

\textstyle{\underset{MP_{i}}{\vdash}}$$\textstyle{A}$$\textstyle{B}

Theorem 21**.**

I_{p3}:\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 51.21489pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-48.4526pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern-26.96022pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-26.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-26.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-43.73839pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-43.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-43.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 8.4526pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern 29.94499pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 29.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern 13.16682pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 12.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-6.05556pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFA_{I}**

\textstyle{A}$$\textstyle{B}

\textstyle{R_{8i}}$$\textstyle{B}$$\textstyle{\vdash}$$\textstyle{B}$$\textstyle{\underset{R_{2}}{\vdash}}$$\textstyle{B}$$\textstyle{A},\textstyle{A}$$\textstyle{B}

\textstyle{R_{8i}}$$\textstyle{A}$$\textstyle{\vdash}$$\textstyle{B}$$\textstyle{\underset{E_{\bot}}{\vdash}}$$\textstyle{A}$$\textstyle{A}$$\textstyle{\underset{MP_{i}}{\vdash}}$$\textstyle{E_{\vee}}

$\textstyle{B}$

$\textstyle{A}$

$\textstyle{B}$

\textstyle{A}$$\textstyle{\vdash}

Theorem 22**.**

\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 51.21489pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-48.4526pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern-26.96022pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-26.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-26.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-43.73839pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-43.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern-43.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 8.4526pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern 29.94499pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 29.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 13.16682pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 12.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-6.05556pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFA_{I}**

$\textstyle{B}$

$\textstyle{A}$

$\textstyle{B}$

\textstyle{A}$$\textstyle{\underset{I_{p3}}{\vdash}}

\textstyle{B}$$\textstyle{A}$$\textstyle{\underset{E_{p}}{\vdash}}

Some of the demonstrated theorems suggest the change of the basic rules of $ALFA_{I}$ by those, given its simplicity, because it allows to obtain a simpler system to handle and of better geometric appearance. Next we present the $ALFA_{Io}$ system that results from changing the rules $I_{\neg},E_{\bot},E_{\neg}$ of $ALFA_{I}$ for the new theorems $I_{p1},E_{p2},I_{p3}$.

3.2 Deductive $ALFA_{Io}$ system

System’s axiom

System’s deductive rules

A)Conserved rules:

$MP_{i},I_{\vee},R_{8i},R_{0},E_{\vee},R_{2}$.

B)New rules:

[TABLE]

$ALFA_{Io}$ is an $GEI$ system whose rules propose new geomorphic content compared to other existential graphic systems. The $E_{p}$ rule is a clear example of this, since it can be stated as: any single dotted closed curve can be closed (complete); With which we have to go from an implication of two-graphs to it’s equivalent in terms of negation and conjunction, it is enough to close the dotted curves. In an analogous way, it happens with $I_{p3}$, where the passage from the disjunction of two graphs to their implication derives from closing one of the semi-dotted curves and opening (the opposite of closing) the other semi-dotted curve. In this way, a simple management system is obtained with high geomorphic value.

$ALFA_{Io}$ is equivalent to $ALFA_{I}$, this is proved by demonstrating that $I_{\neg},E_{\bot},E_{\neg}$ are deductions of the first.

3.2.1 Deductions in $ALFA_{Io}$

Theorem 23**.**

I_{c}:\quad\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 18.49432pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-6.75pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 40.90521pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 50.15521pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 49.90521pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 22.39705pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}}\in ALFA_{Io}**

\textstyle{A}$$\textstyle{A}$$\textstyle{\underset{R_{2}}{\vdash}}$$\textstyle{R_{8i}}$$\textstyle{A}$$\textstyle{A}

\textstyle{A}$$\textstyle{\vdash}$$\textstyle{\underset{E_{p}}{\vdash}}

Theorem 24**.**

$E_{\bot}\in ALFA_{Io}$**

$\textstyle{A}$

$\textstyle{\underset{I_{\vee}}{\vdash}}$

$\textstyle{A}$

$\textstyle{\underset{I_{p3}}{\vdash}}$

$\textstyle{A}$

\textstyle{\underset{I_{c}}{\vdash}}$$\textstyle{A}$$\textstyle{\underset{MP_{i}}{\vdash}}

Theorem 25**.**

$R_{5}^{{}^{\prime}}\in ALFA_{Io}$**

$R_{5}^{{}^{\prime}}$ is a particular case of $R_{5}$, rule that is spoken of in the first section.

\textstyle{A}$$\textstyle{A}$$\textstyle{B}

\textstyle{AB}$$\textstyle{A}$$\textstyle{\underset{I_{p2}}{\vdash}}$$\textstyle{B}$$\textstyle{\underset{MP_{i}}{\vdash}}

Theorem 26**.**

$I_{\neg}\in ALFA_{Io}$**

\textstyle{A}$$\textstyle{\underset{I_{p2}}{\vdash}}$$\textstyle{A}

Theorem 27**.**

$E_{\neg}\in ALFA_{Io}$**

\textstyle{A}$$\textstyle{\underset{E_{p}}{\vdash}}$$\textstyle{A}$$\textstyle{\underset{I_{c}}{\vdash}}$$\textstyle{A}$$\textstyle{\underset{R_{5}^{{}^{\prime}}}{\vdash}}$$\textstyle{A}

The previous theorems prove the equivalence between $ALFA_{Io}$ and $ALFA_{I}$. Now it remains to answer a question: Is it possible to obtain a system of existential graphs equivalent to the $CPC$ of which $ALFA_{Io}$ is a sub-system of?

We will then deduce those $ALFAo$ rules that belong to $ALFA_{Io}$.

Theorem 28**.**

$R_{5}\in ALFA_{Io}$**

\textstyle{B}$$\textstyle{AB}$$\textstyle{A}$$\textstyle{\underset{R_{5}^{{}^{\prime}}}{\vdash}}$$\textstyle{A}$$\textstyle{AB}$$\textstyle{A}$$\textstyle{\underset{R_{2}}{\vdash}}$$\textstyle{A}$$\textstyle{B}$$\textstyle{AB}$$\textstyle{A}$$\textstyle{\vdash}$$\textstyle{R_{0}},

Theorem 29**.**

$R_{7}\in ALFA_{Io}$**

\textstyle{A}$$\textstyle{B}

\textstyle{A}$$\textstyle{B}$$\textstyle{\underset{I_{p2}}{\vdash}}$$\textstyle{A}$$\textstyle{B}$$\textstyle{\underset{E_{p}}{\vdash}}

$R_{7}^{-}$ is deduced in order to facilitate the deduction of the $R_{3}$ rule.

Theorem 30**.**

$R_{7}^{-}\in ALFA_{Io}$**

\textstyle{B}$$\textstyle{A}$$\textstyle{R_{8i}}$$\textstyle{B}$$\textstyle{A}$$\textstyle{\vdash}$$\textstyle{\underset{R_{5}^{{}^{\prime}}}{\vdash}}$$\textstyle{B}$$\textstyle{A}$$\textstyle{B}$$\textstyle{A}$$\textstyle{B}$$\textstyle{A}$$\textstyle{\underset{I_{c}}{\vdash}}$$\textstyle{AB}

Theorem 31**.**

$R_{3}\in ALFA_{Io}$**

\textstyle{A}$$\textstyle{\underset{I_{\vee}}{\vdash}}

$\textstyle{B}$

$\textstyle{A}$

$\textstyle{B}$

\textstyle{A}$$\textstyle{\underset{I_{p3}}{\vdash}}

\textstyle{B}$$\textstyle{A}$$\textstyle{\underset{E_{p}}{\vdash}}

\textstyle{B}$$\textstyle{A}$$\textstyle{\underset{R_{7}^{-}}{\vdash}}

In summary, the rules $R_{0},R_{2},R_{3},R_{5}$ and $R_{7}$ belong to both systems ($ALFAo$ and $ALFA_{Io}$).

3.3 $ALFA_{Io}$ and the $CPC$

Most axiom systems that formalize the $IPC$, are sub-systems of a system that formalizes the $CPC$111See examples of it in [2], fact that can be of great utility when one wishes to compare the intuitionist and classical logic. Based on this, we intend to find a system of existential graphs equivalent to $ALFAo$ of which $ALFA_{Io}$ is sub-system; For this it is necessary to add some rules to $ALFA_{Io}$ in such a way that the new system deducts all of $ALFAo$ rules.

In order to obtain a classic system from the $ALFA_{Io}$ system, the I_{\vee p}:\quad\\ \lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern 51.21489pt\hbox{{\hbox{\framed@@{0.0pt}}}{\hbox{\kern-48.4526pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern-26.96022pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern-26.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-26.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-43.73839pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern-43.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-43.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\framed@@{0.0pt}}}{\hbox{\kern 8.4526pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-24.5pt\hbox{\hbox{\vbox{\vskip 18.0pt\hbox to40.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 18.0pt}}}}}}}{\hbox{\kern 29.94499pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{B}}}}}}{\hbox{\kern 29.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern 29.98839pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern 13.16682pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.41666pt\hbox{\textstyle{A}}}}}}{\hbox{\kern 12.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise-15.5pt\hbox{\hbox{\vbox{\vskip 7.0pt\hbox to14.0pt{\hfill\lx@xy@buildcircle@\hfill}\vskip 7.0pt}}}}}}}{\hbox{\kern 12.91682pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\cirbuild@}}}}}{\hbox{\kern-6.05556pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise-3.47223pt\hbox{\textstyle{\vdash}}}}}}}}}} rule is added.

Now we must prove that the following equivalences are in the $ALFA_{Io}+\{I_{\vee p}\}$ system:

[TABLE]

The first equivalence is given so $I_{p3}\in ALFA_{Io}$ and $I_{\vee p}$ is the added rule. To prove the second equivalence, it is enough to prove that the $E_{p}^{-1}$ rule belongs to the new system, since $E_{p}\in ALFA_{Io}$; which is shown below:

Theorem 32**.**

$E_{p}^{-1}\in ALFA_{Io}+\{I_{\vee p}\}$**

\textstyle{A}$$\textstyle{B}$$\textstyle{\underset{R_{7}}{\vdash}}

\textstyle{B}$$\textstyle{A}

$\textstyle{B}$

$\textstyle{A}$

$\textstyle{\underset{I_{p3}^{-}}{\vdash}}$

$\textstyle{B}$

\textstyle{A}$$\textstyle{\underset{I_{p3}}{\vdash}}

$\textstyle{B}$

\textstyle{A}$$\textstyle{\underset{R_{7}^{-}}{\vdash}}

.

After seeing that in the new system these equivalences are maintained, it’s natural to ask if it’s really classic. To see that it is, we will prove that $ALFA_{Io}+\{I_{\vee p}\}\equiv ALFAo$, for which it should only be shown that all rules of $ALFAo$ are theorems of $ALFA_{Io}+\{I_{\vee p}\}$.

Theorem 33**.**

$R_{6}\in ALFA_{Io}+\{I_{\vee p}\}$**

\textstyle{A}$$\textstyle{A}$$\textstyle{\underset{E_{p}^{-}}{\vdash}}$$\textstyle{B}$$\textstyle{\underset{MP_{i}}{\vdash}}

In the following deduction $R_{6}$ is used as theorem of the $ALFA_{Io}+\{I_{\vee p}\}$ system.

Theorem 34**.**

$R_{4}\in ALFA_{Io}+\{I_{\vee p}\}$**

\textstyle{A}$$\textstyle{C}$$\textstyle{BC}$$\textstyle{\underset{E_{p}}{\vdash}}$$\textstyle{A}$$\textstyle{C}$$\textstyle{BC}

\textstyle{R_{8i}}$$\textstyle{A}$$\textstyle{C}$$\textstyle{B}$$\textstyle{\vdash}$$\textstyle{B}$$\textstyle{C}$$\textstyle{\underset{R_{2}}{\vdash}}$$\textstyle{B}$$\textstyle{C}$$\textstyle{A}$$\textstyle{\underset{R_{6}}{\vdash}}$$\textstyle{C}$$\textstyle{A}$$\textstyle{B}$$\textstyle{A}$$\textstyle{C}$$\textstyle{B}$$\textstyle{\underset{R_{5}}{\vdash}}$$\textstyle{A}$$\textstyle{C}

The rules $R_{0},R_{2},R_{3},R_{5}$ y $R_{7}$ belong to $ALFA_{Io}$, therefore, also to $ALFA_{Io}+\{I_{\vee p}\}$, and the rules $R_{4}$ and $R_{6}$ belong to $ALFA_{Io}+\{I_{\vee p}\}$. It remains to be seen that $R_{8}$ is deductible from this system, proving that it is immediate considering the equivalences between the graphs developed previously.

In conclusion, $ALFA_{Io}+\{I_{\vee p}\}$ and $ALFAo$ are equivalent, except that the first one has more symbols than the second.

4 The $GEI$ of Arnold Oostra

Arnold Oostra presents a system of intuitionist existential graphs in [3]. In this article Oostra introduces the system of graphs mentioned as a proposal for formalization of the intuitionist logic, using diagrams that appear in the manuscripts of Charles S. Peirce. This $GEI$ system differs from the one presented in the previous chapter to a large extent, as will be seen in the following section. It is recommended to refer to the article to understand in depth the proposal made by Oostra.

4.1 Differences between $ALFA_{Io}$ and the $GEI-Oostra$

Earlier it had been suggested that $ALFA_{Io}$ could be considered as the intuitionist version of $ALFAo$ and $GEI-Oostra$ as the intuitionistic version of $alfa$. Thus, it is expected that the differences between $ALFAo$ and $alfa$ will also be preserved as differences of $ALFA_{Io}$ with respect to $GEI-Oostra$. In fact, some are maintained, others are not: for the first case, no deductive rule of $ALFA_{Io}$ is defined in function of the parity of the cuts, and the symmetries of the $ALFAo_{I}$ rules is understood in a different way then the $GEI-Oostra$ system; In the second, $ALFAo_{I}$ rules are not sub-rules of the $GEI-Oostra$ rules.

In addition to the previous differences, there are the differences of the primitive symbols of each system:

The $ALFAo_{I}$ primitive symbols are the ones of $ALFAo$ and the cuts y

The $GEI-Oostra$ primitive symbols are the ones of the $alfa$ system, the curls and the loops

Derived from these choices of the primitive symbols of each system, come the differences corresponding to the representations for implication and disjunction:

Implication and disjunction of two graphs in $ALFA_{Io}$: , .

Implication and disjunction of two graphs in $GEI-Oostra$: , .

$R_{o}$ is a basic $ALFA_{Io}$ rule stated explicitly as the system’s rule, meanwhile in $GEI-Oostra$ no, because in this,the rule is used in the meta-lenguage.

In conclusion, an $ALFAo$ style $GEI$ system was obtained that satisfies all expectations desired in this text. Now all that remains is to continue the work by investigating: the intermediate logics and the existential graphs; the extension of $ALFAo$ and $ALFA_{Io}$ to the predicate calculus and the modal logic in the sense that $beta$ and $gamma$ are $alfa$; and to study $ALFA_{Io}$ in a topological sense taking into account the relations of the intuitionist logic and the topology, considering the cuts dotted as open and the rules interpreted as the calculus of the closure of a cut. In this context, it is expected, with the conclusion of this work, to generate more questions and problems that were attempted to solve.

5 Acknowledgments

We thank the office of the Vice President of Research at the Technological University of Pereira for funding this research through the project, 3-17-2.