Mostrar código-fonte de Lógica/Cálculo Quantificacional Clássico/Identidade e Símbolos Funcionais



=Símbolos de identidade e funcionais <math>(CQC_f^=)</math>=

==Tablôs Semânticos para o <math>CQC_f^=</math>==

==Dedução Natural no <math>CQC_f^=</math>==

==Formalização de sistemas pelo <math>CQC_f^=</math>==
===Fomalização da Aritmética pelo <math>CQC_f^=</math>===
:'''N1''' <math> \forall x\; \left (sx\ne x\right )</math>
:'''N2''' <math> \forall x\;\forall y\; \left (sx=sy\to x=y\right )</math>
:'''N3''' <math> \forall x\; \left (x+0=x\right )</math>
:'''N4''' <math> \forall x\;\forall y\; \left (x+sy=s\left (x+y\right )\right )</math>
:'''N5''' <math> \forall x\; \left (x\times 0=0\right )</math>
:'''N6''' <math> \forall x\;\forall y\; \left (x\times sy=\left (x\times y\right )+x\right )</math>
:'''N7''' <math> \forall x\;\neg \left (x < \;0\right )</math>
:'''N8''' <math> \forall x\;\forall y\; \left (x< \;sy\leftrightarrow \;\left (x< \;y\lor \;x=y\right )\right )</math>
:'''N9''' <math> \forall x\;\forall y\; \left (x< \;y\lor \;x=y\lor \;y< \;x\right )</math>

{{Esboço/Matemática}}

{{AutoCat}}