Open main menu
Logic Wiki
Search
Exercícios de semântica formal para a Lógica de Primeira Ordem Clássica
Read in another language
Watch this page
Edit
Revision as of 10:48, 17 October 2020 by
Greati
(
talk
|
contribs
)
(
diff
)
← Older revision
| Latest revision (diff) | Newer revision → (diff)
Contents
1
Validade global de sequentes
1.1
(
∃
x
)
(
∀
y
)
φ
{\displaystyle (\exists x)(\forall y)\varphi }
▷
(
∀
y
)
(
∃
x
)
φ
{\displaystyle (\forall y)(\exists x)\varphi }
1.2
(
∀
y
)
(
∃
x
)
φ
{\displaystyle (\forall y)(\exists x)\varphi }
▶
(
∃
x
)
(
∀
y
)
φ
{\displaystyle (\exists x)(\forall y)\varphi }
1.3
(
∀
x
:
P
)
φ
{\displaystyle (\forall x{:}P)\varphi }
◁▷
¬
(
∃
x
:
P
)
¬
φ
{\displaystyle \neg (\exists x{:}P)\neg \varphi }
1.4
(
∀
x
)
(
φ
→
ψ
)
{\displaystyle (\forall x)(\varphi \to \psi )}
▷
(
∀
x
)
φ
→
(
∀
x
)
ψ
{\displaystyle (\forall x)\varphi \to (\forall x)\psi }
1.5
(
∀
x
)
φ
→
(
∀
x
)
ψ
{\displaystyle (\forall x)\varphi \to (\forall x)\psi }
▶
(
∀
x
)
(
φ
→
ψ
)
{\displaystyle (\forall x)(\varphi \to \psi )}
2
Validade de sequentes em interpretações particulares
2.1
w
≈
x
f
(
y
g
z
)
{\displaystyle w\approx x{\mathsf {f}}(y{\mathsf {g}}z)}
▷
I
w
≈
(
x
f
y
)
g
(
x
f
z
)
{\displaystyle ^{\mathfrak {I}}w\approx (x{\mathsf {f}}y){\mathsf {g}}(x{\mathsf {f}}z)}
3
Correção de regras
3.1
Regras para o símbolo de igualdade
3.2
(
∀
E
)
Γ
⊢
(
∀
x
)
φ
/
Γ
⊢
φ
[
x
↦
t
]
{\displaystyle \mathrm {(\forall E)} \Gamma \vdash (\forall x)\varphi /\Gamma \vdash \varphi [x\mapsto t]}
3.3
(
∀
I
)
Γ
⊢
φ
[
x
↦
y
]
/
Γ
⊢
(
∀
x
)
φ
{\displaystyle \mathrm {(\forall I)} \Gamma \vdash \varphi [x\mapsto y]/\Gamma \vdash (\forall x)\varphi }
4
Para reflexão
5
Veja também
6
Links externos
Validade global de sequentes
(
∃
x
)
(
∀
y
)
φ
{\displaystyle (\exists x)(\forall y)\varphi }
▷
(
∀
y
)
(
∃
x
)
φ
{\displaystyle (\forall y)(\exists x)\varphi }
(
∀
y
)
(
∃
x
)
φ
{\displaystyle (\forall y)(\exists x)\varphi }
▶
(
∃
x
)
(
∀
y
)
φ
{\displaystyle (\exists x)(\forall y)\varphi }
(
∀
x
:
P
)
φ
{\displaystyle (\forall x{:}P)\varphi }
◁▷
¬
(
∃
x
:
P
)
¬
φ
{\displaystyle \neg (\exists x{:}P)\neg \varphi }
(
∀
x
)
(
φ
→
ψ
)
{\displaystyle (\forall x)(\varphi \to \psi )}
▷
(
∀
x
)
φ
→
(
∀
x
)
ψ
{\displaystyle (\forall x)\varphi \to (\forall x)\psi }
(
∀
x
)
φ
→
(
∀
x
)
ψ
{\displaystyle (\forall x)\varphi \to (\forall x)\psi }
▶
(
∀
x
)
(
φ
→
ψ
)
{\displaystyle (\forall x)(\varphi \to \psi )}
Validade de sequentes em interpretações particulares
w
≈
x
f
(
y
g
z
)
{\displaystyle w\approx x{\mathsf {f}}(y{\mathsf {g}}z)}
▷
I
w
≈
(
x
f
y
)
g
(
x
f
z
)
{\displaystyle ^{\mathfrak {I}}w\approx (x{\mathsf {f}}y){\mathsf {g}}(x{\mathsf {f}}z)}
Correção de regras
Regras para o símbolo de igualdade
(
∀
E
)
Γ
⊢
(
∀
x
)
φ
/
Γ
⊢
φ
[
x
↦
t
]
{\displaystyle \mathrm {(\forall E)} \Gamma \vdash (\forall x)\varphi /\Gamma \vdash \varphi [x\mapsto t]}
(
∀
I
)
Γ
⊢
φ
[
x
↦
y
]
/
Γ
⊢
(
∀
x
)
φ
{\displaystyle \mathrm {(\forall I)} \Gamma \vdash \varphi [x\mapsto y]/\Gamma \vdash (\forall x)\varphi }
Para reflexão
Veja também
Introdução Computacional à Lógica Matemática
Links externos
Lógica de Primeira Ordem
Interpretação (lógica)
Valoração (lógica)
▷ 
▶ 
◁▷ 
▷ 
▶ 
▷
![{\displaystyle \mathrm {(\forall E)} \Gamma \vdash (\forall x)\varphi /\Gamma \vdash \varphi [x\mapsto t]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/39311bbdd0dcbe859d3a8986410d5837ce6020ef)
![{\displaystyle \mathrm {(\forall I)} \Gamma \vdash \varphi [x\mapsto y]/\Gamma \vdash (\forall x)\varphi }](https://wikimedia.org/api/rest_v1/media/math/render/svg/737e13dc6958222367205de9b61b5abac8154403)