A kommutativitás bizonyítása - A részletezés jobbra nyitható!
Értelmezés sikertelen (ismeretlen „\textup” függvény): {\displaystyle \begin{array}{rcll} PA\cup \{(0+x)=x\} & \vdash & (0+x)=x & \textup{premissza levezethető} \\ PA\cup \{(0+x)=x\} & \vdash & s(0+x)=sx & \textup{elsőrendű logikai törvény}\\ PA\cup \{(0+x)=x\} & \vdash & s(0+x)=(0+sx) & \textup{3. axióma} \\ PA\cup \{(0+x)=x\} & \vdash & (0+sx)=sx & \textup{Az azonosságokból } \\ PA & \vdash & (0+x)=x\rightarrow (0+sx)=sx & \textup{Dedukciótétel} \\ PA & \vdash & \forall x ((0+x)=x\rightarrow 0+sx=sx) & \textup{Univerzális generalizáció}\\ PA & \vdash & F_x[0] \rightarrow \forall x( F \rightarrow F_x[sx]) \rightarrow F & \textup{7. axióma} \\ PA & \vdash & ((0+x)=x)_x[0]\forall x ((0+x)=x ((0+x)=x)_x[sx])((0+x)=x) & F:=(0+x=x) \\ PA & \vdash & (0+0)=0\rightarrow \forall x ((0+x)=x \rightarrow (0+sx)=sx )\rightarrow (0+x)=x & \textup{behelyettesítés} \\ PA & \vdash & (0+0)=0 & \textup{3. axióma} \\ PA & \vdash & \forall x ( (0+x)=x\rightarrow (0+sx)=sx)\rightarrow (0+x)=x & \textup{modus ponens}\\ PA & \vdash & (0+x)=x & \textup{modus ponens}\\ PA & \vdash & (x+0)=x & \textup{3.axióma}\\ PA & \vdash & (0+x)=(x+0) & \textup{Az azonosságokból } \\ PA & \vdash & \forall x (0+x)=(x+0) & \textup{Univerzális generalizáció}\\ PA \cup \{ (x+y)=(y+x) \}&\vdash & (x+y)=(y+x) & \textup{premissza levezethető} \\ PA \cup \{ (x+y)=(y+x) \}&\vdash & s(x+y)=s(y+x) & \textup{Elsőrendű logikai törvény} \\ PA \cup \{ (x+y)=(y+x) \}&\vdash & s(x+y)=(x+sy) & \textup{4. axióma}\\ PA\cup \{ (x+y)=(y+x) \}&\vdash & s(y+x)=(y+sx) & \textup{4. axióma}\\ PA\cup \{ (x+y)=(y+x) \}&\vdash & (x+sy)=(sy+x) & \textup{Az azonosságokból} \\ PA &\vdash & (x+y)=(y+x) \rightarrow (x+sy)=(sy+x) & \textup{Dedukciótétel} \\ PA &\vdash & \forall x (x+y)=(y+x) \rightarrow (x+sy)=(sy+x) & \textup{Univerzális generalizáció} \\ PA &\vdash & \forall x (x+y)=(y+x) \rightarrow \forall x ((x+ sy= (sy+x)) & \textup{2.axióma} \\ PA &\vdash & \forall y \forall x((x+y)=(y+x)\rightarrow \forall x (x+sy)=(sy+x) & \textup{Univerzális generalizáció} \\ PA & \vdash & F_x[0] \rightarrow \forall x( F \rightarrow F_x[ sx] \rightarrow F & \textup{7. axióma} \\ PA & \vdash & (\forall x (x+y)=(y+x))_x[0] \rightarrow \forall x( \forall x (x+y)=(y+x) \rightarrow (\forall x (x+y)=(y+x))_x[ sx] \rightarrow \forall x (x+y)=(y+x) & F :=\forall x (x+y)=(y+x)\\ PA & \vdash & \forall x (0+y)=(y+0) \rightarrow \forall x( \forall x (x+y)=(y+x) \rightarrow \forall x (sx+y)=(y+sx)) \rightarrow \forall x (x+y)=(y+x) & \textup{terminuscsere} \\ PA & \vdash & \forall y \forall x (x+y)=(y+x) \rightarrow \forall x (x+sy)=(sy+x) \rightarrow \forall x (x+y)=(y+x) & \textup{modus ponens}\\ PA & \vdash & \forall x (x+y)=(y+x) & \textup{modus ponens}\\ PA & \vdash & \forall y \forall x (x+y)=(y+x) & \textup{Univerzális generalizáció}\\ PA & \vdash & \forall x \forall y (x+y)=(y+x) & \textup{kvantorcsere} \\ \end{array} }
Peano-aritmetikai fogalmak és egyebek.
Σ
1
{\displaystyle \scriptstyle {\Sigma _{1}}}
formulák osztálya
Bázis
0
=
s
u
∈
Σ
1
{\displaystyle \scriptstyle {0=su\in \Sigma _{1}}}
s
u
=
v
∈
Σ
1
{\displaystyle \scriptstyle {su=v\in \Sigma _{1}}}
u
+
v
=
w
∈
Σ
1
{\displaystyle \scriptstyle {u+v=w\in \Sigma _{1}}}
u
⋅
v
=
w
∈
Σ
1
{\displaystyle \scriptstyle {u\cdot v=w\in \Sigma _{1}}}
Rekurzió
F
,
G
∈
Σ
1
⇒
(
F
∧
G
)
∈
Σ
1
{\displaystyle \scriptstyle {F,G\in \Sigma _{1}\Rightarrow (F\land G)\in \Sigma _{1}}}
F
,
G
∈
Σ
1
⇒
(
F
∨
G
)
∈
Σ
1
{\displaystyle \scriptstyle {F,G\in \Sigma _{1}\Rightarrow (F\vee G)\in \Sigma _{1}}}
F
∈
Σ
1
⇒
∃
x
F
∈
Σ
1
{\displaystyle \scriptstyle {F\in \Sigma _{1}\Rightarrow \exists xF\in \Sigma _{1}}}
F
∈
Σ
1
⇒
(
∀
x
<
y
)
F
∈
Σ
1
{\displaystyle \scriptstyle {F\in \Sigma _{1}\Rightarrow (\forall x<y)F\in \Sigma _{1}}}
F
,
G
∈
Σ
1
⇒
(
F
∧
G
)
∈
Σ
1
{\displaystyle \scriptstyle {F,G\in \Sigma _{1}\Rightarrow (F\land G)\in \Sigma _{1}}}
P
A
⊢
∀
x
∀
y
(
x
+
y
)
=
(
y
+
x
)
{\displaystyle \scriptstyle {PA\vdash \forall x\forall y(x+y)=(y+x)}}
P
A
⊢
∀
x
∀
y
∀
z
(
(
x
+
y
)
+
z
)
=
(
x
+
(
y
+
z
)
)
{\displaystyle \scriptstyle {PA\vdash \forall x\forall y\forall z((x+y)+z)=(x+(y+z))}}
P
A
⊢
∀
x
∀
y
∀
z
(
x
⋅
(
y
+
z
)
)
=
(
(
x
⋅
y
)
+
(
x
⋅
z
)
)
{\displaystyle \scriptstyle {PA\vdash \forall x\forall y\forall z(x\cdot (y+z))=((x\cdot y)+(x\cdot z))}}
P
A
⊢
∀
x
∀
y
∀
z
(
(
x
⋅
y
)
⋅
z
)
=
(
x
⋅
(
y
⋅
z
)
)
{\displaystyle \scriptstyle {PA\vdash \forall x\forall y\forall z((x\cdot y)\cdot z)=(x\cdot (y\cdot z))}}
P
A
⊢
∀
x
∀
y
(
x
⋅
y
)
=
(
y
⋅
x
)
{\displaystyle \scriptstyle {PA\vdash \forall x\forall y(x\cdot y)=(y\cdot x)}}
P
A
⊢
∀
x
∀
y
(
x
+
y
)
=
(
y
+
x
)
{\displaystyle \scriptstyle {PA\vdash \forall x\forall y(x+y)=(y+x)}}
Ha i meg j egyenlő k -val, akkor
P
A
⊢
(
i
+
j
)
=
k
{\displaystyle \scriptstyle {PA\vdash (i+j)=k}}
, ahol
i
{\displaystyle \scriptstyle {i}}
-ben i darab
s
{\displaystyle \scriptstyle {s}}
jel van, stb.
Ha i -szer j egyenlő k -val, akkor
P
A
⊢
(
i
⋅
j
)
=
k
{\displaystyle \scriptstyle {PA\vdash (i\cdot j)=k}}
, ahol
i
{\displaystyle \scriptstyle {i}}
-ben i darab
s
{\displaystyle \scriptstyle {s}}
jel van, stb.
Ha
t
{\displaystyle \scriptstyle {t}}
egy változót nem tartalmazó terminus és i -t jelöli, akkor
P
A
⊢
t
=
i
{\displaystyle \scriptstyle {PA\vdash t=i}}
Ha
t
{\displaystyle \scriptstyle {t}}
és
t
′
{\displaystyle \scriptstyle {t'}}
változót nem tartalmazó terminusok és ugyanazt jelölik, akkor
P
A
⊢
t
=
t
′
{\displaystyle \scriptstyle {PA\vdash t=t'}}
x
≤
y
⟺
d
e
f
∃
z
(
x
+
z
=
y
)
{\displaystyle \scriptstyle {x\leq y\iff _{def}\exists z(x+z=y)}}
x
<
y
⟺
d
e
f
x
≤
y
∧
x
≠
y
{\displaystyle \scriptstyle {x<y\iff _{def}x\leq y\land x\neq y}}
x
>
y
⟺
d
e
f
¬
x
≤
y
{\displaystyle \scriptstyle {x>y\iff _{def}\lnot x\leq y}}
x
≥
y
⟺
d
e
f
¬
x
<
y
{\displaystyle \scriptstyle {x\geq y\iff _{def}\lnot x<y}}
P
A
⊢
∀
x
¬
x
<
0
{\displaystyle \scriptstyle {PA\vdash \forall x\lnot x<0}}
⋁
{
x
=
j
:
{\displaystyle \scriptstyle {\bigvee \{x=j:}}
j < i
}
{\displaystyle \scriptstyle {\}}}
P
A
⊢
(
∀
x
(
∀
y
(
y
<
x
→
F
(
y
)
)
→
F
(
x
)
)
→
F
(
x
)
)
{\displaystyle \scriptstyle {PA\vdash (\forall x(\forall y(y<x\rightarrow F(y))\rightarrow F(x))\rightarrow F(x))}}
P
A
⊢
(
F
(
x
)
→
∃
x
(
F
(
x
)
∧
∀
y
(
y
<
x
→
¬
F
(
y
)
)
)
)
{\displaystyle \scriptstyle {PA\vdash (F(x)\rightarrow \exists x(F(x)\land \forall y(y<x\rightarrow \lnot F(y))))}}
P
A
⊢
¬
x
<
x
{\displaystyle \scriptstyle {PA\vdash \lnot x<x}}
P
A
⊢
(
(
x
<
y
∧
y
<
z
)
→
x
<
z
)
{\displaystyle \scriptstyle {PA\vdash ((x<y\land y<z)\rightarrow x<z)}}
P
A
⊢
(
(
x
<
y
∨
x
=
y
)
∨
x
>
y
)
{\displaystyle \scriptstyle {PA\vdash ((x<y\vee x=y)\vee x>y)}}
P
A
⊢
(
x
<
y
→
(
x
+
z
)
<
(
y
+
z
)
)
{\displaystyle \scriptstyle {PA\vdash (x<y\rightarrow (x+z)<(y+z))}}
P
A
⊢
(
(
x
<
y
∧
0
<
z
)
→
(
x
⋅
z
)
<
(
y
⋅
z
)
)
{\displaystyle \scriptstyle {PA\vdash ((x<y\land 0<z)\rightarrow (x\cdot z)<(y\cdot z))}}
Σ
1
{\displaystyle \scriptstyle {\Sigma _{1}}}
formulák osztálya
Bázis
0
=
s
u
∈
Σ
1
s
u
=
v
∈
Σ
1
u
+
v
=
w
∈
Σ
1
u
⋅
v
=
w
∈
Σ
1
{\displaystyle \scriptstyle {\begin{array}{r}\scriptstyle {0=su\in \Sigma _{1}}\\\scriptstyle {su=v\in \Sigma _{1}}\\\scriptstyle {u+v=w\in \Sigma _{1}}\\\scriptstyle {u\cdot v=w\in \Sigma _{1}}\end{array}}}
Rekurzió
F
,
G
∈
Σ
1
⇒
(
F
∧
G
)
∈
Σ
1
F
,
G
∈
Σ
1
⇒
(
F
∨
G
)
∈
Σ
1
F
∈
Σ
1
⇒
∃
x
F
∈
Σ
1
F
∈
Σ
1
⇒
(
∀
x
<
y
)
F
∈
Σ
1
{\displaystyle \scriptstyle {\begin{array}{rcr}\scriptstyle {F,G\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {(F\land G)\in \Sigma _{1}}\\\scriptstyle {F,G\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {(F\vee G)\in \Sigma _{1}}\\\scriptstyle {F\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {\exists xF\in \Sigma _{1}}\\\scriptstyle {F\in \Sigma _{1}}&\scriptstyle {\Rightarrow }&\scriptstyle {(\forall x<y)F\in \Sigma _{1}}\end{array}}}
*Ha i kisebb, mint j , akkor
P
A
⊢
i
<
j
{\displaystyle \scriptstyle {PA\vdash i<j}}
Ha i más, mint j , akkor
P
A
⊢
i
≠
j
{\displaystyle \scriptstyle {PA\vdash i\neq j}}
Ha i nem kisebb, mint j , akkor
P
A
⊢
¬
i
<
j
{\displaystyle \scriptstyle {PA\vdash \lnot i<j}}
Egy
F
(
x
1
,
x
2
,
…
x
n
,
y
)
{\displaystyle \scriptstyle {F(x_{1},x_{2},\dots x_{n},y)}}
formula pszeudoterminus , ha
P
A
⊢
∃
!
y
F
(
x
1
,
x
2
,
…
x
n
,
y
)
{\displaystyle \scriptstyle {PA\vdash \exists !yF(x_{1},x_{2},\dots x_{n},y)}}
. A pszeudoterminusokat így szokás jelölni:
f
(
x
1
,
x
2
,
…
x
n
)
{\displaystyle \scriptstyle {f(x_{1},x_{2},\dots x_{n})}}
. Minden pszeudoterminus egy n -argumentumú függvényt definiál.
A
(
f
(
x
1
,
x
2
,
…
x
n
)
)
⟺
d
e
f
∃
y
(
F
(
x
1
,
x
2
,
…
x
n
,
y
)
∧
A
(
y
)
)
{\displaystyle \scriptstyle {A(f(x_{1},x_{2},\dots x_{n}))\iff _{def}\exists y(F(x_{1},x_{2},\dots x_{n},y)\land A(y))}}
Ha
F
∈
Σ
1
{\displaystyle \scriptstyle {F\in \Sigma _{1}}}
igaz, akkor
P
A
⊢
F
{\displaystyle \scriptstyle {PA\vdash F}}
F
∈
Π
1
⟺
d
e
f
¬
F
∈
Σ
1
{\displaystyle \scriptstyle {F\in \Pi _{1}\iff _{def}\lnot F\in \Sigma _{1}}}
Δ
=
Σ
1
∩
Π
1
{\displaystyle \scriptstyle {\Delta =\Sigma _{1}\cap \Pi _{1}}}
Δ
{\displaystyle \scriptstyle {\Delta }}
tartalmazza az összes atomi formulát és a
t
<
t
′
{\displaystyle \scriptstyle {t<t'}}
,
u
|
v
{\displaystyle \scriptstyle {u|v}}
,
I
r
r
e
d
u
c
i
b
l
e
(
p
)
{\displaystyle \scriptstyle {Irreducible(p)}}
,
R
e
l
a
t
i
v
e
l
y
P
r
i
m
e
(
a
,
b
)
{\displaystyle \scriptstyle {RelativelyPrime(a,b)}}
alakú formulákat, zárt a Boole-műveletekre, a korlátos kvantifikációkra és a pszeudoterminusok bármely helyettesítésére.
d
|
x
⟺
d
e
f
∃
q
(
q
⋅
d
)
=
x
{\displaystyle \scriptstyle {d|x\iff _{def}\exists q(q\cdot d)=x}}
P
A
⊢
(
∃
q
(
q
⋅
d
)
=
x
→
∃
q
(
q
≤
x
∧
(
q
⋅
d
)
=
x
)
)
{\displaystyle \scriptstyle {PA\vdash (\exists q(q\cdot d)=x\rightarrow \exists q(q\leq x\land (q\cdot d)=x))}}
P
A
⊢
d
|
d
{\displaystyle \scriptstyle {PA\vdash d|d}}
P
A
⊢
(
(
d
|
x
∧
x
|
y
)
→
d
|
y
)
{\displaystyle \scriptstyle {PA\vdash ((d|x\land x|y)\rightarrow d|y)}}
P
A
⊢
(
d
|
x
→
(
d
|
(
x
+
y
)
↔
d
|
y
)
)
{\displaystyle \scriptstyle {PA\vdash (d|x\rightarrow (d|(x+y)\leftrightarrow d|y))}}
P
A
⊢
(
d
≠
0
→
∃
q
∃
r
(
(
(
x
=
q
⋅
d
+
r
∧
r
<
d
)
∧
∀
q
′
∀
r
′
(
(
x
=
(
q
′
⋅
d
)
+
r
′
∧
r
<
d
)
→
(
q
=
q
′
∧
r
=
r
′
)
)
)
)
)
{\displaystyle \scriptstyle {PA\vdash (d\neq 0\rightarrow \exists q\exists r(((x=q\cdot d+r\land r<d)\land \forall q'\forall r'((x=(q'\cdot d)+r'\land r<d)\rightarrow (q=q'\land r=r')))))}}
R
m
(
x
,
d
,
r
)
⟺
d
e
f
(
(
r
<
d
∧
∃
q
x
=
(
q
⋅
d
)
+
r
)
∨
(
d
=
0
∧
r
=
x
)
)
{\displaystyle \scriptstyle {Rm(x,d,r)\iff _{def}((r<d\land \exists qx=(q\cdot d)+r)\vee (d=0\land r=x))}}
R
m
(
x
,
d
,
r
)
∈
Σ
{\displaystyle \scriptstyle {Rm(x,d,r)\in \Sigma }}
és pszeudoterminus
P
A
⊢
r
m
(
x
,
0
=
x
{\displaystyle \scriptstyle {PA\vdash rm(x,0}=x}
P
A
⊢
(
d
|
x
↔
r
m
(
x
,
d
)
=
0
)
{\displaystyle \scriptstyle {PA\vdash (d|x\leftrightarrow rm(x,d)=0)}}
P
A
⊢
r
m
(
x
+
y
d
,
d
)
=
r
m
(
x
,
d
)
{\displaystyle \scriptstyle {PA\vdash rm(x+yd,d)=rm(x,d)}}
P
A
⊢
y
≤
x
→
∃
!
z
x
=
y
+
z
{\displaystyle \scriptstyle {PA\vdash y\leq x\rightarrow \exists !zx=y+z}}
M
o
n
u
s
(
x
,
y
,
z
⟺
d
e
f
(
x
=
y
+
z
∨
(
x
<
y
∧
z
=
0
)
)
{\displaystyle \scriptstyle {Monus(x,y,z\iff _{def}(x=y+z\vee (x<y\land z=0))}}
x
−
y
=
z
⟺
d
e
f
m
o
n
u
s
(
x
,
y
)
=
z
{\displaystyle \scriptstyle {x-y=z\iff _{def}monus(x,y)=z}}
I
r
r
e
d
u
c
i
b
l
e
(
p
)
⟺
d
e
f
(
p
≠
1
∧
∀
d
(
d
|
p
→
(
d
=
1
∨
d
=
p
)
)
)
{\displaystyle \scriptstyle {Irreducible(p)\iff _{def}(p\neq 1\land \forall d(d|p\rightarrow (d=1\vee d=p)))}}
P
r
i
m
e
(
p
)
⟺
d
e
f
(
p
≠
1
→
∀
x
∀
y
(
p
|
x
y
→
(
p
|
x
∨
p
|
y
)
)
)
{\displaystyle \scriptstyle {Prime(p)\iff _{def}(p\neq 1\rightarrow \forall x\forall y(p|xy\rightarrow (p|x\vee p|y)))}}
P
A
⊢
(
I
r
r
e
d
u
c
i
b
l
e
(
2
)
∧
∀
x
(
I
r
r
e
d
u
c
i
b
l
e
(
x
)
→
x
≥
2
)
)
{\displaystyle \scriptstyle {PA\vdash (Irreducible(2)\land \forall x(Irreducible(x)\rightarrow x\geq 2))}}
P
A
⊢
∀
x
(
x
>
1
→
∃
p
(
I
r
r
e
d
u
c
i
b
l
e
(
p
)
∧
p
|
x
)
)
{\displaystyle \scriptstyle {PA\vdash \forall x(x>1\rightarrow \exists p(Irreducible(p)\land p|x))}}
R
e
l
a
t
i
v
e
l
y
P
r
i
m
e
(
a
,
b
)
⟺
d
e
f
∀
d
(
(
d
|
a
∧
d
|
b
)
→
d
=
1
)
{\displaystyle \scriptstyle {RelativelyPrime(a,b)\iff _{def}\forall d((d|a\land d|b)\rightarrow d=1)}}
P
A
⊢
R
e
l
a
t
i
v
e
l
y
P
r
i
m
e
(
a
,
b
)
↔
¬
∃
x
(
I
r
r
e
d
u
c
i
b
l
e
(
x
)
∧
(
x
|
a
∧
x
|
b
)
)
{\displaystyle \scriptstyle {PA\vdash RelativelyPrime(a,b)\leftrightarrow \lnot \exists x(Irreducible(x)\land (x|a\land x|b))}}
P
A
⊢
∀
a
∀
b
(
(
(
a
>
1
∧
b
>
1
)
∧
R
e
l
a
t
i
v
e
l
y
P
r
i
m
e
(
a
,
b
)
)
→
∃
x
∃
y
a
x
+
1
=
b
y
)
{\displaystyle \scriptstyle {PA\vdash \forall a\forall b(((a>1\land b>1)\land RelativelyPrime(a,b))\rightarrow \exists x\exists yax+1=by)}}
P
A
⊢
∀
x
(
I
r
r
e
d
u
c
i
b
l
e
(
x
)
→
P
r
i
m
e
(
x
)
)
{\displaystyle \scriptstyle {PA\vdash \forall x(Irreducible(x)\rightarrow Prime(x))}}
tételek S5 -ből
◻
(
A
∨
◻
B
)
→
(
◻
A
∨
◻
B
)
{\displaystyle \scriptstyle {\Box (A\vee \Box B)\rightarrow (\Box A\vee \Box B)}}
◻
(
A
∨
◊
B
)
→
(
◻
A
∨
◊
B
)
{\displaystyle \scriptstyle {\Box (A\vee \Diamond B)\rightarrow (\Box A\vee \Diamond B)}}
◊
(
A
∧
◊
B
)
↔
(
◊
A
∧
◊
B
)
{\displaystyle \scriptstyle {\Diamond (A\land \Diamond B)\leftrightarrow (\Diamond A\land \Diamond B)}}
◊
(
A
∧
◻
B
)
↔
(
◊
A
∧
◻
B
)
{\displaystyle \scriptstyle {\Diamond (A\land \Box B)\leftrightarrow (\Diamond A\land \Box B)}}
◻
(
◻
A
→
◻
B
)
∨
◻
(
◻
B
→
◻
A
)
{\displaystyle \scriptstyle {\Box (\Box A\rightarrow \Box B)\vee \Box (\Box B\rightarrow \Box A)}}
S4-hez szép diagram a modalitások sorrendjéhez.
\[{\Huge \textbf{S4}} \begin{array}{c}\xymatrix{
\Box A \ar[r]\ar[dd]
& \Box \Diamond \Box A \ar[r]\ar[d] & \Diamond \Box A\ar[d]
\\ & \Box \Diamond A \ar[r] & \Diamond \Box \Diamond A\ar[d]
\\ A\ar[rr] && \Diamond A}\end{array}\]
K-s tételek:
◻
(
A
⊃
B
)
⊃
(
◻
A
⊃
◻
B
)
◻
(
p
∧
q
)
≡
(
◻
p
∧
◻
q
)
◻
p
∨
◻
q
)
⊃
◻
(
p
∨
q
)
◊
(
p
∨
q
)
≡
(
◊
p
∨
◊
q
)
◊
(
p
⊃
q
)
≡
(
◻
p
⊃
◊
q
)
◊
(
p
∧
q
)
⊃
(
◊
p
∧
◊
q
)
(
◊
p
∧
◻
q
)
⊃
◊
(
p
∧
q
)
◻
(
p
∨
q
)
⊃
(
◻
p
∨
◊
q
)
{\displaystyle {\begin{array}{l}\Box (A\supset B)\supset (\Box A\supset \Box B)\\\Box (p\land q)\equiv (\Box p\land \Box q)\\\Box p\vee \Box q)\supset \Box (p\vee q)\\\Diamond (p\vee q)\equiv (\Diamond p\vee \Diamond q)\\\Diamond (p\supset q)\equiv (\Box p\supset \Diamond q)\\\Diamond (p\land q)\supset (\Diamond p\land \Diamond q)\\(\Diamond p\land \Box q)\supset \Diamond (p\land q)\\\Box (p\vee q)\supset (\Box p\vee \Diamond q)\end{array}}}
Azaz:
haakkor:
◻
(
A
⊃
B
)
⊃
(
◻
A
⊃
◻
B
)
◊
(
p
⊃
q
)
≡
(
◻
p
⊃
◊
q
)
◊
(
p
⊃
q
)
⊃
(
◊
p
⊃
◊
q
)
{\displaystyle {\begin{array}{l}\Box (A\supset B)\supset (\Box A\supset \Box B)\\\Diamond (p\supset q)\equiv (\Box p\supset \Diamond q)\\\Diamond (p\supset q)\supset (\Diamond p\supset \Diamond q)\end{array}}}
és:
◻
(
p
∧
q
)
≡
(
◻
p
∧
◻
q
)
◊
(
p
∧
q
)
⊃
(
◊
p
∧
◊
q
)
(
◊
p
∧
◻
q
)
⊃
◊
(
p
∧
q
)
{\displaystyle {\begin{array}{l}\\\Box (p\land q)\equiv (\Box p\land \Box q)\\\Diamond (p\land q)\supset (\Diamond p\land \Diamond q)\\(\Diamond p\land \Box q)\supset \Diamond (p\land q)\end{array}}}
vagy:
◻
p
∨
◻
q
)
⊃
◻
(
p
∨
q
)
◊
(
p
∨
q
)
≡
(
◊
p
∨
◊
q
)
◻
(
p
∨
q
)
⊃
(
◻
p
∨
◊
q
)
{\displaystyle {\begin{array}{l}\\\Box p\vee \Box q)\supset \Box (p\vee q)\\\Diamond (p\vee q)\equiv (\Diamond p\vee \Diamond q)\\\Box (p\vee q)\supset (\Box p\vee \Diamond q)\end{array}}}
érvényes formulák K -ból
∧
{\displaystyle \scriptstyle {\land }}
◻
(
A
∧
B
)
↔
(
◻
A
∧
◻
B
)
{\displaystyle \scriptstyle {\Box (A\land B)\leftrightarrow (\Box A\land \Box B)}}
◊
(
A
∧
B
)
→
(
◊
A
∧
◊
B
)
{\displaystyle \scriptstyle {\Diamond (A\land B)\rightarrow (\Diamond A\land \Diamond B)}}
(
◻
A
∧
◊
B
)
→
◊
(
A
∧
B
)
{\displaystyle \scriptstyle {(\Box A\land \Diamond B)\rightarrow \Diamond (A\land B)}}
∨
{\displaystyle \scriptstyle {\lor }}
◻
A
∨
◻
B
)
→
◻
(
A
∨
B
)
{\displaystyle \scriptstyle {\Box A\vee \Box B)\rightarrow \Box (A\vee B)}}
◊
(
A
∨
B
)
↔
(
◊
A
∨
◊
B
)
{\displaystyle \scriptstyle {\Diamond (A\vee B)\leftrightarrow (\Diamond A\vee \Diamond B)}}
◻
(
A
∨
B
)
→
(
◻
A
∨
◊
B
)
{\displaystyle \scriptstyle {\Box (A\vee B)\rightarrow (\Box A\vee \Diamond B)}}
→
{\displaystyle \scriptstyle {\rightarrow }}
◻
(
A
→
B
)
→
(
◻
A
→
◻
B
)
{\displaystyle \scriptstyle {\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B)}}
◊
(
A
→
B
)
↔
(
◻
A
→
◊
B
)
{\displaystyle \scriptstyle {\Diamond (A\rightarrow B)\leftrightarrow (\Box A\rightarrow \Diamond B)}}
◊
(
A
→
B
)
→
(
◊
A
→
◊
B
)
{\displaystyle \scriptstyle {\Diamond (A\rightarrow B)\rightarrow (\Diamond A\rightarrow \Diamond B)}}
A
⊃
B
◻
A
⊃
◻
B
A
≡
B
◻
A
≡
◻
B
A
⊃
B
◊
A
⊃
◊
B
{\displaystyle {\frac {A\supset B}{\Box A\supset \Box B}}\qquad {\frac {A\equiv B}{\Box A\equiv \Box B}}\qquad {\frac {A\supset B}{\Diamond A\supset \Diamond B}}}
Ez meg azért érvényes K-ban, mert nincsenek ilyen alakú tételei:
◊
A
A
◻
◊
A
A
{\displaystyle {\frac {\Diamond A}{A}}\qquad {\frac {\Box \Diamond A}{A}}}
modalitásredukciók:
Ezek lennének a lehetségesek
◊
p
≡
◻
◊
p
◻
p
≡
◊
◻
p
◊
p
≡
◊
◊
p
◻
p
≡
◻
◻
p
{\displaystyle {\begin{array}{l}\\\Diamond p\equiv \Box \Diamond p\\\Box p\equiv \Diamond \Box p\\\Diamond p\equiv \Diamond \Diamond p\\\Box p\equiv \Box \Box p\end{array}}}
Ezek vannak T-ben:
◻
◊
p
⊃
◊
p
◻
p
⊃
◊
◻
p
◊
p
⊃
◊
◊
p
◻
◻
p
⊃
◻
p
{\displaystyle {\begin{array}{l}\Box \Diamond p\supset \Diamond p\\\Box p\supset \Diamond \Box p\\\Diamond p\supset \Diamond \Diamond p\\\Box \Box p\supset \Box p\end{array}}}
A hiányzók egyelőre nem tudjuk hol érvényesek:
◊
p
⊃
◻
◊
p
◊
◻
p
⊃
◻
p
◊
◊
p
⊃
◊
p
◻
p
⊃
◻
◻
p
{\displaystyle {\begin{array}{l}\Diamond p\supset \Box \Diamond p\\\Diamond \Box p\supset \Box p\\\Diamond \Diamond p\supset \Diamond p\\\Box p\supset \Box \Box p\end{array}}}
K-ban viszont igazak a következő következtetések:
◊
◊
p
⊃
◊
p
◻
p
⊃
◻
◻
p
{\displaystyle {\begin{array}{l}\Diamond \Diamond p\supset \Diamond p\\\hline \hline \Box p\supset \Box \Box p\end{array}}}
◊
p
⊃
◻
◊
p
◊
◻
p
⊃
◻
p
{\displaystyle {\begin{array}{l}\Diamond p\supset \Box \Diamond p\\\hline \hline \Diamond \Box p\supset \Box p\end{array}}}
T-ben pedig még ez is:
◊
p
⊃
◻
◊
p
◻
p
⊃
◻
◻
p
{\displaystyle {\frac {\Diamond p\supset \Box \Diamond p}{\Box p\supset \Box \Box p}}}
Ja meg még ez a három is:
◻
A
⊃
A
A
⊃
◊
A
◻
A
⊃
◊
A
{\displaystyle {\begin{array}{l}\Box A\supset A\\A\supset \Diamond A\\\Box A\supset \Diamond A\end{array}}}
K4-ben meg igaz:
◻
◊
◻
◊
A
≡
◻
◊
A
{\displaystyle \Box \Diamond \Box \Diamond A\equiv \Box \Diamond A}