Difference between revisions of "Exercícios de semântica formal para a Lógica de Primeira Ordem Clássica"

Latest revision as of 10:48, 17 October 2020

Validade global de sequentes

$(\exists x)(\forall y)\varphi$ ▷ $(\forall y)(\exists x)\varphi$

$(\forall y)(\exists x)\varphi$ ▶ $(\exists x)(\forall y)\varphi$

$(\forall x{:}P)\varphi$ ◁▷ $\neg (\exists x{:}P)\neg \varphi$

$(\forall x)(\varphi \to \psi )$ ▷ $(\forall x)\varphi \to (\forall x)\psi$

$(\forall x)\varphi \to (\forall x)\psi$ ▶ $(\forall x)(\varphi \to \psi )$

Validade de sequentes em interpretações particulares

$w\approx x{\mathsf {f}}(y{\mathsf {g}}z)$ ▷ $^{\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

$\mathrm {(\forall E)} \Gamma \vdash (\forall x)\varphi /\Gamma \vdash \varphi [x\mapsto t]$

$\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

@@ Line 25: / Line 25: @@
 === Regras para o símbolo de igualdade ===
 : {{#ev:youtube|RTlRlxsRzjA|||||start=239&loop=1}}
+=== <math>\mathrm{(\forall E)} \Gamma \vdash (\forall x)\varphi / \Gamma \vdash \varphi[x \mapsto t]</math> ===
+: {{#ev:youtube|zRZmfBlAiv0|||||start=490&loop=1}}
+=== <math>\mathrm{(\forall I)} \Gamma \vdash \varphi[x \mapsto y] / \Gamma \vdash (\forall x)\varphi </math> ===
+: {{#ev:youtube|zRZmfBlAiv0|||||start=721&loop=1}}
 == Para reflexão ==

Difference between revisions of "Exercícios de semântica formal para a Lógica de Primeira Ordem Clássica"

Latest revision as of 10:48, 17 October 2020

Contents

Validade global de sequentes

$(\exists x)(\forall y)\varphi$ ▷ $(\forall y)(\exists x)\varphi$

$(\forall y)(\exists x)\varphi$ ▶ $(\exists x)(\forall y)\varphi$

$(\forall x{:}P)\varphi$ ◁▷ $\neg (\exists x{:}P)\neg \varphi$

$(\forall x)(\varphi \to \psi )$ ▷ $(\forall x)\varphi \to (\forall x)\psi$

$(\forall x)\varphi \to (\forall x)\psi$ ▶ $(\forall x)(\varphi \to \psi )$

Validade de sequentes em interpretações particulares

$w\approx x{\mathsf {f}}(y{\mathsf {g}}z)$ ▷ $^{\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

$\mathrm {(\forall E)} \Gamma \vdash (\forall x)\varphi /\Gamma \vdash \varphi [x\mapsto t]$

$\mathrm {(\forall I)} \Gamma \vdash \varphi [x\mapsto y]/\Gamma \vdash (\forall x)\varphi$

Para reflexão

Veja também

Links externos

Navigation menu

Personal tools

Namespaces

Variants

Views

More

Search

Navigation

Tools

Difference between revisions of "Exercícios de semântica formal para a Lógica de Primeira Ordem Clássica"

Latest revision as of 10:48, 17 October 2020

Contents

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

Links externos

Navigation menu

Search

$(\exists x)(\forall y)\varphi$ ▷ $(\forall y)(\exists x)\varphi$

$(\forall y)(\exists x)\varphi$ ▶ $(\exists x)(\forall y)\varphi$

$(\forall x{:}P)\varphi$ ◁▷ $\neg (\exists x{:}P)\neg \varphi$

$(\forall x)(\varphi \to \psi )$ ▷ $(\forall x)\varphi \to (\forall x)\psi$

$(\forall x)\varphi \to (\forall x)\psi$ ▶ $(\forall x)(\varphi \to \psi )$

$w\approx x{\mathsf {f}}(y{\mathsf {g}}z)$ ▷ $^{\mathfrak {I}}w\approx (x{\mathsf {f}}y){\mathsf {g}}(x{\mathsf {f}}z)$

$\mathrm {(\forall E)} \Gamma \vdash (\forall x)\varphi /\Gamma \vdash \varphi [x\mapsto t]$

$\mathrm {(\forall I)} \Gamma \vdash \varphi [x\mapsto y]/\Gamma \vdash (\forall x)\varphi$