7760 lines
126 KiB
Plaintext
7760 lines
126 KiB
Plaintext
#LyX 2.3 created this file. For more info see http://www.lyx.org/
|
||
\lyxformat 544
|
||
\begin_document
|
||
\begin_header
|
||
\save_transient_properties true
|
||
\origin unavailable
|
||
\textclass memoir
|
||
\begin_preamble
|
||
\usepackage{pxfonts}
|
||
\usepackage{tikz}
|
||
\usepackage[usenames,dvipsnames]{pstricks}
|
||
\usepackage{epsfig}
|
||
\usepackage{pst-grad} % For gradients
|
||
\usepackage{pst-plot} % For axes
|
||
\usepackage[space]{grffile} % For spaces in paths
|
||
\usepackage{etoolbox} % For spaces in paths
|
||
\makeatletter % For spaces in paths
|
||
\patchcmd\Gread@eps{\@inputcheck#1 }{\@inputcheck"#1"\relax}{}{}
|
||
\makeatother
|
||
\newtheorem*{problem*}{\protect\problemname}
|
||
\providecommand{\problemname}{Problema}
|
||
\usepackage[dvipsnames]{xcolor} % para cores
|
||
\makeatletter
|
||
\hypersetup{
|
||
%pagebackref=true,
|
||
pdftitle={\@title},
|
||
pdfauthor={\@author},
|
||
% pdfsubject={\imprimirpreambulo},
|
||
pdfcreator={LaTeX with abnTeX2},
|
||
pdfkeywords={abnt}{latex}{abntex}{abntex2}{livro},
|
||
colorlinks=true, % false: boxed links; true: colored links
|
||
linkcolor=blue, % color of internal links
|
||
citecolor=blue, % color of links to bibliography
|
||
filecolor=magenta, % color of file links
|
||
urlcolor=blue,
|
||
bookmarksdepth=4
|
||
}
|
||
\makeatother
|
||
\end_preamble
|
||
\use_default_options true
|
||
\begin_modules
|
||
theorems-ams
|
||
theorems-chap
|
||
\end_modules
|
||
\maintain_unincluded_children false
|
||
\language brazilian
|
||
\language_package default
|
||
\inputencoding auto
|
||
\fontencoding T1
|
||
\font_roman "lmodern" "default"
|
||
\font_sans "default" "default"
|
||
\font_typewriter "lmodern" "default"
|
||
\font_math "auto" "auto"
|
||
\font_default_family default
|
||
\use_non_tex_fonts false
|
||
\font_sc false
|
||
\font_osf false
|
||
\font_sf_scale 100 100
|
||
\font_tt_scale 100 100
|
||
\use_microtype false
|
||
\use_dash_ligatures true
|
||
\graphics default
|
||
\default_output_format default
|
||
\output_sync 0
|
||
\bibtex_command default
|
||
\index_command default
|
||
\paperfontsize default
|
||
\spacing onehalf
|
||
\use_hyperref true
|
||
\pdf_bookmarks false
|
||
\pdf_bookmarksnumbered false
|
||
\pdf_bookmarksopen false
|
||
\pdf_bookmarksopenlevel 1
|
||
\pdf_breaklinks true
|
||
\pdf_pdfborder true
|
||
\pdf_colorlinks true
|
||
\pdf_backref page
|
||
\pdf_pdfusetitle false
|
||
\pdf_quoted_options "hidelinks,pdfcreator={LaTeX via pandoc}"
|
||
\papersize default
|
||
\use_geometry false
|
||
\use_package amsmath 2
|
||
\use_package amssymb 2
|
||
\use_package cancel 0
|
||
\use_package esint 1
|
||
\use_package mathdots 0
|
||
\use_package mathtools 0
|
||
\use_package mhchem 0
|
||
\use_package stackrel 0
|
||
\use_package stmaryrd 0
|
||
\use_package undertilde 0
|
||
\cite_engine basic
|
||
\cite_engine_type default
|
||
\biblio_style plain
|
||
\use_bibtopic false
|
||
\use_indices false
|
||
\paperorientation portrait
|
||
\suppress_date true
|
||
\justification true
|
||
\use_refstyle 0
|
||
\use_minted 0
|
||
\backgroundcolor #ffffff
|
||
\fontcolor #000000
|
||
\index Index
|
||
\shortcut idx
|
||
\color #008000
|
||
\end_index
|
||
\secnumdepth 1
|
||
\tocdepth 1
|
||
\paragraph_separation indent
|
||
\paragraph_indentation default
|
||
\is_math_indent 0
|
||
\math_numbering_side default
|
||
\quotes_style english
|
||
\dynamic_quotes 0
|
||
\papercolumns 1
|
||
\papersides 2
|
||
\paperpagestyle default
|
||
\tracking_changes false
|
||
\output_changes false
|
||
\html_math_output 0
|
||
\html_css_as_file 0
|
||
\html_be_strict false
|
||
\end_header
|
||
|
||
\begin_body
|
||
|
||
\begin_layout Title
|
||
Caixas e diamantes: uma introdução aberta à lógica modal
|
||
\end_layout
|
||
|
||
\begin_layout Author
|
||
Remixado por Richard Zach
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
frontmatter
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
tableofcontents*
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Chapter
|
||
Prefácio
|
||
\end_layout
|
||
|
||
\begin_layout Chapter
|
||
Introdução
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Lógicas modais são extensões da lógica clássica por meio da introdução dos
|
||
operadores
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
(
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
caixa
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
) e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
(
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
diamante
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
), que se anexam a fórmulas.
|
||
Intuitivamente,
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
pode ser lido como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
necessariamente
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit,$
|
||
\end_inset
|
||
|
||
como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
possivelmente.
|
||
Assim
|
||
\begin_inset Formula $\square p$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é necessariamente verdadeira
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit p$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é possivelmente verdadeira
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que necessidade e possibilidade são noções metafísicas fundamentais,
|
||
lógica modal é, obviamente, de grande interesse filosófico.
|
||
Ela permite a formalização de princípios metafísicos tais como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
(se
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é necessária, então ela é verdadeira) ou
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\diamondsuit p\rightarrow\square\diamondsuit p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
(se
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é possível, ela é necessariamente possível).
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Os operadores
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
são
|
||
\emph on
|
||
intensionais
|
||
\emph default
|
||
.
|
||
Isto significa que a verdade ou falsidade de
|
||
\begin_inset Formula $\square A$
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Formula $\diamondsuit A$
|
||
\end_inset
|
||
|
||
não dependem apenas da verdade ou falsidade de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
Um operador que não é intensional é extensional.
|
||
A negação é extensional:
|
||
\begin_inset Formula $\neg A$
|
||
\end_inset
|
||
|
||
é verdadeiro se e somente (sse)
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é falso; assim, o valor de verdade de
|
||
\begin_inset Formula $\neg A$
|
||
\end_inset
|
||
|
||
depende somente do valor de verdade de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
não são dessa forma.
|
||
O valor de verdade de
|
||
\begin_inset Formula $\square A$
|
||
\end_inset
|
||
|
||
ou de
|
||
\begin_inset Formula $\diamondsuit A$
|
||
\end_inset
|
||
|
||
depende também do significado de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
Embora a semântica verofuncional seja suficiente para lidar com operadores
|
||
extensionais, operadores intensionais como
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
requerem um tipo diferente de semântica.
|
||
Uma dessas semânticas que toma um lugar central neste livro é a semântica
|
||
relacional (também chamada semântica de mundos possíveis ou semântica de
|
||
Kripke).
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A lógica que corresponde à interpretação de
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
necessariamente
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
tem uma semântica que é é relativamente simples: em vez de atribuir valores
|
||
de verdade às variáveis proposicionais, uma interpretação
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
atribui a um conjunto de
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
mundos
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
a elas — intuitivamente, aqueles mundos em que
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é interpretado como verdadeiro.
|
||
Com base em uma tal interpretação, podemos definir uma relação de satisfação.
|
||
A definição desta relação de satisfação torna
|
||
\begin_inset Formula $\square A$
|
||
\end_inset
|
||
|
||
satisfeita em um mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é satisfeita em
|
||
\emph on
|
||
todos
|
||
\emph default
|
||
os mundos:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},v\Vdash A$
|
||
\end_inset
|
||
|
||
, para todos os mundos
|
||
\begin_inset Formula $v$
|
||
\end_inset
|
||
|
||
.
|
||
Isto corresponde à ideia de Leibniz segundo a qual o que é necessariamente
|
||
verdadeiro é o que é verdadeiro em qualquer mundo possível.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Necessariamente
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
não é a única maneira de se interpretar o operador
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
, mas é a padrão —
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
necessariamente
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
possivelmente
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
são as então chamadas modalidades
|
||
\emph on
|
||
aléticas
|
||
\emph default
|
||
.
|
||
Em outras interpretações,
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
é lido como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
é conhecido (por alguma pessoa
|
||
\emph on
|
||
A
|
||
\emph default
|
||
) que
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
, como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
alguma pessoa
|
||
\emph on
|
||
A
|
||
\emph default
|
||
acredita que
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
, como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
deveria ser o caso que
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
ou como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
sempre será verdadeiro que
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Estas são, respectivamente, modalidades epistêmicas, doxásticas, deônticas
|
||
e temporais.
|
||
Interpretações diferentes de
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
farão com que uma mesma fórmula seja logicamente verdadeira em uma interpretaçã
|
||
o e não logicamente verdadeira em outra; da mesma forma, uma certa inferência
|
||
pode ser válida em uma interpretação e inválida na outra.
|
||
Por exemplo, tudo que é necessário é verdadeiro ou tudo que é conhecido
|
||
é verdadeiro, assim
|
||
\begin_inset Formula $\square A\rightarrow A$
|
||
\end_inset
|
||
|
||
é uma verdade lógica nas interpretações alética e epistêmica.
|
||
Por outro lado, nem tudo que é acredito ou nem tudo que deveria ser o caso
|
||
é, de fato, o caso.
|
||
Dessa forma,
|
||
\begin_inset Formula $\square A\rightarrow A$
|
||
\end_inset
|
||
|
||
não é uma verdade nas interpretações doxástica ou deôntica.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A fim de lidar com diferentes interpretações dos operadores modais, a semântica
|
||
é estendida por meio de uma relação entre mundos, a então chamada relação
|
||
de acessibilidade.
|
||
Então
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},v\Vdash A$
|
||
\end_inset
|
||
|
||
para todos os mundos
|
||
\begin_inset Formula $v$
|
||
\end_inset
|
||
|
||
que são acessíveis a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
A semântica resultante é bastante versátil e poderosa, e a ideia básica
|
||
pode ser usada para fornecer interpretações semânticas para lógicas baseadas
|
||
em outros operadores intensionais.
|
||
Uma dessas lógicas é a lógica intuicionista, uma lógica construtiva baseada
|
||
no ramo da matemática construtiva de L.
|
||
E.
|
||
J.
|
||
Brouwer.
|
||
Lógica intuicionista é filosoficamente interessante por esta razão — ela
|
||
desempenha um papel importante na explicação construtiva da matemática
|
||
[in constructive accounts of mathematics].
|
||
Michael Dummett, influente filósofo inglês do século 20, propôs a lógica
|
||
intuicionista como uma lógica superior à lógica clássica.
|
||
Uma outra aplicação dos modelos relacionais é quando eles são usados como
|
||
semântica para condicionais subjuntivos ou contrafactuais, uma abordagem
|
||
que foi desbravada por Robert Stalnaker e David K.
|
||
Lewis.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Este livro é uma introdução à sintaxe, à semântica e à teoria da prova de
|
||
lógicas intensionais.
|
||
Ela trata apenas de lógicas proposicionais, embora edições futuras também
|
||
lidarão com lógicas de predicados.
|
||
O material é dividido em três partes: a primeira parte lida com lógicas
|
||
modais normais.
|
||
Estas são lógicas com os operadores
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
.
|
||
Discutimos a sintaxe delas, modelos relacionais e noções semânticas baseadas
|
||
nesses modelos (tais como validade e consequência) e sistemas de provas
|
||
(tanto sistemas axiomáticos como tablôs).
|
||
Estabelecemos alguns resultados sobre estas lógicas tais como correção
|
||
e completude dos sistemas de provas considerados e discutimos algumas construçõ
|
||
es modelo-teóricos [model-theoretic construction] tais como filtrações.
|
||
A segunda parte trada da lógica intuicionista.
|
||
Aqui discutimos dedução natural e derivações axiomáticas, semânticas relacionai
|
||
s e topológica e correção e completude dos sistemas de provas.
|
||
A terceira parte lida com a semântica Lewis-Stalnaker dos condicionais
|
||
contrafactuais.
|
||
O apêndice discute algumas ideias e resultados da teoria de conjuntos e
|
||
da teoria das relações que são cruciais para a semântica relacional assim
|
||
como recapitula a sintaxe, semântica e teoria da prova da lógica proposicional
|
||
clássica.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
mainmatter
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Part
|
||
Lógicas modais normais
|
||
\end_layout
|
||
|
||
\begin_layout Chapter
|
||
Sintaxe e semântica das lógicas normais modais
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Introdução
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Lógica modal lida com proposições
|
||
\emph on
|
||
modais
|
||
\emph default
|
||
e com as relações de acarretamento [entailment] que ocorre entre elas.
|
||
Exemplos de proposições modais são os seguintes:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
É necessário que
|
||
\begin_inset Formula $2+2=4$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
É necessariamente possível que chova amanhã
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Se é necessariamente possível que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
, então é possível que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Possibilidade e necessidade não são as únicas modalidades: outros conectivos
|
||
unários são também classificados como modalidades, por exemplo,
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
deveria ser o caso que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Dana sabe que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Dana acredita que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A primeira aparição da lógica modal ocorre no livro
|
||
\emph on
|
||
Da Interpretação
|
||
\emph default
|
||
de Aristóteles: ele foi o primeiro a perceber que necessidade implica possibili
|
||
dade, mas não vice-versa; que possibilidade e necessidade são interdefiníveis;
|
||
que se
|
||
\begin_inset Formula $A\wedge B$
|
||
\end_inset
|
||
|
||
é possivelmente verdadeira, então
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é possivelmente verdadeira e
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
é possivelmente verdadeira, mas não inversamente; e que se
|
||
\begin_inset Formula $A\rightarrow B$
|
||
\end_inset
|
||
|
||
é necessária, então se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é necessária, então
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
é necessária.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A primeira abordagem moderna da lógica modal foi o trabalho de C.
|
||
I.
|
||
Lewis, que culminou no livro
|
||
\emph on
|
||
Lógica Simbólica
|
||
\emph default
|
||
(1932) de Lewis e Langford.
|
||
Lewis e Langford estavam insatisfeitos com a representação da implicação
|
||
por meio do condicional material:
|
||
\begin_inset Formula $A\rightarrow B$
|
||
\end_inset
|
||
|
||
é um substituto pobre para
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
A implica B
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Em vez disso, eles propuseram caracterizar implicação como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Necessariamente, se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
, simbolizada como
|
||
\begin_inset Formula $A\strictif B$
|
||
\end_inset
|
||
|
||
.
|
||
Tentando isolar diferentes propriedades, Lewis identificou cinco sistema
|
||
modais diferentes,
|
||
\series bold
|
||
S1
|
||
\series default
|
||
,
|
||
\series bold
|
||
S2
|
||
\series default
|
||
,
|
||
\series bold
|
||
S3
|
||
\series default
|
||
,
|
||
\series bold
|
||
S4
|
||
\series default
|
||
,
|
||
\series bold
|
||
S5
|
||
\series default
|
||
, sendo as duas últimas ainda usadas.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A abordagem de Lewis e Langford foi puramente sintática: eles identificaram
|
||
axiomas e regras razoáveis e investigaram o que era derivável por esses
|
||
meios.
|
||
Uma abordagem semântica continuou indescritível por muito tempo [A semantic
|
||
approach remained elusive for a long time], até que uma primeira tentativa
|
||
foi feita por Rudolf Carnap em
|
||
\emph on
|
||
Significado e Necessidade
|
||
\emph default
|
||
(1947) usando a noção de
|
||
\emph on
|
||
descrição de estado
|
||
\emph default
|
||
, isto é, uma coleção de sentenças atômicas (aquelas que são
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
verdadeiras
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
neste estado de descrição).
|
||
Depois de apresentar a definição de verdade para sentenças arbitrárias
|
||
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
[After lifting the truth definition to arbitrary sentences A], Carnap define
|
||
A como sendo
|
||
\emph on
|
||
necessariamente verdadeira
|
||
\emph default
|
||
, se ela é verdadeira em todas as descrições de estado.
|
||
A abordagem de Carnap não poderia lidar com modalidades
|
||
\emph on
|
||
iteradas
|
||
\emph default
|
||
, já que sentenças da forma
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Possivelmente é necessário que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é possível
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
sempre se reduzem à modalidade mais interna [innermost].
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
O maior avanço [breakthrough] na semântica modal veio com artigo
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Um teorema da completude na lógica modal
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
(JSL 1959) de Saul Kripke.
|
||
Kripke baseou o seu trabalho na ideia de Leibniz segundo a qual um enunciado
|
||
é necessariamente verdadeiro se ele é verdadeiro
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
em todos os mundos possíveis
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Esta ideia , entretanto, sofre das mesmas desvantagens [drawbacks] que
|
||
a de Carnap, já que a verdade do enunciado em um mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
(ou em uma descrição de estado
|
||
\begin_inset Formula $s$
|
||
\end_inset
|
||
|
||
) não depende de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
absolutamente.
|
||
Assim Kripke assumiu que os mundos estão relacionados por meio de uma
|
||
\emph on
|
||
relação de acessibilidade
|
||
\emph default
|
||
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
e que um enunciado da forma
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Necessariamente
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
é verdadeira em um mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeiro em todos os mundos
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
acessíveis a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Semânticas que ofereceram alguma versão desta abordagem são chamadas semênticas
|
||
de Kripke e possibilitaram o desenvolvimento turbulento [tumultuous development
|
||
] das lógicas modais (no plural).
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Quando interpretada pelas semânticas de Kripke, lógica modal mostra-nos
|
||
como são as estruturas relacionais
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
de dentro
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Uma estrutura relacional é exatamente um conjunto abastecido com uma relação
|
||
binária (por exemplo, o conjunto de estudantes na sala de aula ordenados
|
||
pelo numeração da carteira de identidade (ou cpf) é uma estrutura relacional).
|
||
Mas, de fato, estruturas relacionais estão disponíveis [come in] em todos
|
||
os tipos de domínios: além da possibilidade relativa dos estados do mundo,
|
||
podemos ter estados epistêmicos de algum agente relacionado por possibilidade
|
||
epistêmica ou ter estados de um sistema dinâmico com as transições de estado
|
||
deles, etc.
|
||
Lógica modal pode ser usada para modelar todos estes: a primeira estrutura
|
||
nos dá lógica modal ordinária, alética; as outras nos são lógica epistêmica,
|
||
lógica dinâmica, etc.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Focamos em um ângulo particular, conhecido pelos lógicos modais como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
teoria da correspondência
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Uma das mais significantes descobertas iniciais de Kripke é que muitas
|
||
propriedades da relação de acessibilidade
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
(se ela é transitiva, simétrica, etc) podem ser caracterizadas
|
||
\emph on
|
||
na própria linguagem modal
|
||
\emph default
|
||
por meio de
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
esquemas modais
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
apropriados.
|
||
Lógicos modais dizem, por exemplo, que a reflexividade de
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
corresponde
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
ao esquema
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
Se necessariamente
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
Exploramos principalmente a teoria da correspondência de alguns sistemas
|
||
clássicos de lógica modal (por exemplo,
|
||
\series bold
|
||
S4
|
||
\series default
|
||
e
|
||
\series bold
|
||
S5
|
||
\series default
|
||
) obtidos por meio da combinação dos esquemas D, T, B, 4 e 5.
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
A linguagem da lógica modal básica
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
A linguagem básica da lógica modal contém
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
A constante proposicional para falsidade
|
||
\begin_inset Formula $\bot$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Um conjunto infinito e enumerável de variáveis proposicionais:
|
||
\begin_inset Formula $p_{0},p_{1},p_{2},\ldots$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Os conectivos proposicionais:
|
||
\begin_inset Formula $\neg$
|
||
\end_inset
|
||
|
||
(negação),
|
||
\begin_inset Formula $\wedge$
|
||
\end_inset
|
||
|
||
(conjunção),
|
||
\begin_inset Formula $\vee$
|
||
\end_inset
|
||
|
||
(disjunção),
|
||
\begin_inset Formula $\rightarrow$
|
||
\end_inset
|
||
|
||
(condicional)
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
O operador modal
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
O operador modal
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
|
||
\emph on
|
||
Fórmulas
|
||
\emph default
|
||
da linguagem modal básica são indutivamente definidas como se segue
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\bot$
|
||
\end_inset
|
||
|
||
é uma fórmula atômica
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Qualquer variável proposicional
|
||
\begin_inset Formula $p_{i}$
|
||
\end_inset
|
||
|
||
é uma fórmula (atômica)
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
são fórmulas, então
|
||
\begin_inset Formula $(A\wedge B)$
|
||
\end_inset
|
||
|
||
é uma fórmula.
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
são fórmulas, então
|
||
\begin_inset Formula $(A\vee B)$
|
||
\end_inset
|
||
|
||
é uma fórmula.
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
são fórmulas, então
|
||
\begin_inset Formula $(A\rightarrow B)$
|
||
\end_inset
|
||
|
||
é uma fórmula.
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é uma fórmula, então
|
||
\begin_inset Formula $\square A$
|
||
\end_inset
|
||
|
||
é uma fórmula
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é uma fórmula, então
|
||
\begin_inset Formula $\diamondsuit A$
|
||
\end_inset
|
||
|
||
é uma fórmula
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
Nenhuma outra expressão é uma fórmula
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Fórmulas costruidas usando operadores definidos devem ser compreendidas
|
||
como se segue
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
⊤ abrevia
|
||
\begin_inset Formula $\neg$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\bot$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
↔
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
abrevia
|
||
\begin_inset Formula $(A\rightarrow B)$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\wedge$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $(B\rightarrow A)$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Se a fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
não contém
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
, dizemos que ela é modalmente livre [modal-free]
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Substituição simultânea
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Uma instância de uma fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é o resultado da substituição de todas as ocorrências de uma variável proposici
|
||
onal em
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
por alguma outra fórmula.
|
||
Referir-nos-emos frequentemente às instâncias das fórmulas tanto ao discutir
|
||
validade com ao discutir derivabilidade.
|
||
Portanto é útil definir a noção precisamente.
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Sejam
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
uma fórmula modal em que todas as variáveis proposicionais estão entre
|
||
|
||
\begin_inset Formula $p_{1},\ldots,p_{n}$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $D_{1},\ldots,D_{n}$
|
||
\end_inset
|
||
|
||
fórmulas também modais, definimos
|
||
\begin_inset Formula $A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
como o resultado de substituir simultaneamente cada um dos
|
||
\begin_inset Formula $p_{i}$
|
||
\end_inset
|
||
|
||
por
|
||
\begin_inset Formula $D_{i}$
|
||
\end_inset
|
||
|
||
em
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
Formalmente, isto é uma definição por indução sobre [a complexidade de]
|
||
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\bot$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $\bot$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv q$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $q$
|
||
\end_inset
|
||
|
||
, dado que
|
||
\begin_inset Formula $q\not\equiv p_{i}$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $i=1,\ldots,n$
|
||
\end_inset
|
||
|
||
).
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv p_{i}$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $D_{i}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\neg B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $\neg B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\wedge C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\wedge C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\vee C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\vee C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\rightarrow C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\rightarrow C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\leftrightarrow C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $(B[D_{1}/p_{1},\dots,D_{n}/p_{n}]\leftrightarrow C[D_{1}/p_{1},\dots,D_{n}/p_{n}])$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\square B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $\square B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\diamondsuit B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $\diamondsuit B[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
A fórmula
|
||
\begin_inset Formula $A[D_{1}/p_{1},\dots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é chamada uma instância de substituição de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Example
|
||
Suponha que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
seja
|
||
\begin_inset Formula $p_{1}\rightarrow\square(p_{1}\wedge p_{2})$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $D_{1}$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\diamondsuit(p_{2}\rightarrow p_{3})$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $D_{2}$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\neg\square p_{1}$
|
||
\end_inset
|
||
|
||
.
|
||
Então
|
||
\begin_inset Formula $A[D_{1}/p_{1},D_{2}/p_{2}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge\neg\square p_{1})$
|
||
\end_inset
|
||
|
||
.
|
||
Por outro lado,
|
||
\begin_inset Formula $A[D_{2}/p_{1},D_{1}/p_{2}]$
|
||
\end_inset
|
||
|
||
é
|
||
\begin_inset Formula $\neg\square p_{1}\rightarrow\square(\neg\square p_{1}\wedge\diamondsuit(p_{2}\rightarrow p_{3}))$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Note que substituição simultânea não é, em geral, o mesmo que substituição
|
||
iterada, por exemplo, compare
|
||
\begin_inset Formula $A[D_{1}/p_{1},D_{2}/p_{2}]$
|
||
\end_inset
|
||
|
||
acima com
|
||
\begin_inset Formula $(A[D_{1}/p_{1}])[D_{2}/p_{2}]$
|
||
\end_inset
|
||
|
||
que é:
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\align center
|
||
\begin_inset Formula $\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge p_{2})[\neg\square p_{1}/p_{2}]$
|
||
\end_inset
|
||
|
||
, ou seja,
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\align center
|
||
\begin_inset Formula $\diamondsuit(\neg\square p_{1}\rightarrow p_{3})\rightarrow\square(\diamondsuit(\neg\square p_{1}\rightarrow p_{3})\wedge\neg\square p_{1})$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
E também compare com
|
||
\begin_inset Formula $(A[D_{2}/p_{2}])[D_{1}/p_{1}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\align center
|
||
\begin_inset Formula $p_{1}\rightarrow\square(p_{1}\wedge\neg\square p_{1})[\diamondsuit(p_{2}\rightarrow p_{3})/p_{1}]$
|
||
\end_inset
|
||
|
||
, ou seja,
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\align center
|
||
\begin_inset Formula $\diamondsuit(p_{2}\rightarrow p_{3})\rightarrow\square(\diamondsuit(p_{2}\rightarrow p_{3})\wedge\neg\square\diamondsuit(p_{2}\rightarrow p_{3}))$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Modelos relacionais
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
O conceito básico de semântica para lógicas modais normais é o de
|
||
\emph on
|
||
modelo relacional
|
||
\emph default
|
||
.
|
||
O modelo consiste em um conjunto de mundos, que estão relacionados por
|
||
meio de uma
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
|
||
\emph on
|
||
relação de acessibilidade
|
||
\emph default
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
binária, junto com uma atribuição que determina quais variáveis proposicionais
|
||
contam como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
verdadeiras
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
nestes mundos.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Um
|
||
\emph on
|
||
modelo
|
||
\emph default
|
||
para linguagem modal básica é uma tripla ordenada
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
, em que
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $W$
|
||
\end_inset
|
||
|
||
é um conjunto não-vazio de
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
mundos
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
é uma relação de acessibilidade binária sobre
|
||
\begin_inset Formula $W$
|
||
\end_inset
|
||
|
||
e;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $V$
|
||
\end_inset
|
||
|
||
é uma função que atribui a cada variável proposicional
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
um conjunto
|
||
\begin_inset Formula $V(p)$
|
||
\end_inset
|
||
|
||
de mundos possíveis.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
Quando
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
vale, dizemos que
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
|
||
\emph on
|
||
é acessível a partir de
|
||
\emph default
|
||
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Quando
|
||
\begin_inset Formula $w\in V(p)$
|
||
\end_inset
|
||
|
||
, dizemos que
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
|
||
\emph on
|
||
é verdadeira em
|
||
\emph default
|
||
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A grande vantagem da semântica relacional é que modelos podem ser representados
|
||
por meio de diagramas simples, tais como o da Figura
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
ref{fig:simples}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
.
|
||
Mundos são representados por nódulos e o mundo
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
é acessível a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
exatamente quando há uma seta de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
em direção a
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
.
|
||
Além disso, rotulamos um nódulo (mundo) por
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
quando
|
||
\begin_inset Formula $w\in V(p)$
|
||
\end_inset
|
||
|
||
.
|
||
Caso contrário, rotulamos o nódulo por
|
||
\begin_inset Formula $\neg p$
|
||
\end_inset
|
||
|
||
.
|
||
A Figura
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
ref{fig:simples}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
representa o modelo com
|
||
\begin_inset Formula $W=\{w_{1},w_{2},w_{3}\},R=\{<w_{1},w_{2}>,<w_{1},w_{3}>\},V(p)=\{w_{1},w_{2}\}$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $v(q)=\{w_{2}\}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Float figure
|
||
wide false
|
||
sideways false
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
\align center
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psscalebox{.7 .7} % Change this value to rescale the drawing.
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
{
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
begin{pspicture}(0,-3.9)(6.14,3.9)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](0.88,-0.22){0.88}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.64,3.02){0.88}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.62,-3.02){0.88}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.64,-0.32){$w_1$}
|
||
\backslash
|
||
rput[bl](4.54,2.9){$w_2$}
|
||
\backslash
|
||
rput[bl](4.38,-3.2){$w_3$}
|
||
\backslash
|
||
rput[bl](2.04,-0.02){$p$}
|
||
\backslash
|
||
rput[bl](1.94,-0.52){$
|
||
\backslash
|
||
neg q$}
|
||
\backslash
|
||
rput[bl](5.94,3.18){$p$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](5.9,2.56){$q$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](5.74,-2.88){$
|
||
\backslash
|
||
neg p$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](5.74,-3.42){$
|
||
\backslash
|
||
neg q$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(1.64,-0.84)(3.6,-2.5)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(1.52,0.68)(3.66,2.44)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
end{pspicture}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Caption Standard
|
||
|
||
\begin_layout Plain Layout
|
||
Um modelo simples.
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "fig:simples"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Verdade em um mundo
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Qualquer modelo modal determina quais fórmulas modais contam como verdadeiras
|
||
nos mundos dentro do modelo.
|
||
A relação
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
modelo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
faz a fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
verdadeira no mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
é uma noção básica de semântica relacional.
|
||
A relação é definida indutivamente e coincide com a caracterização habitual
|
||
que usa tabelas de verdade para operadores não-modais.
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
|
||
\emph on
|
||
Verdade de uma fórmula A em
|
||
\emph default
|
||
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
em um [modelo]
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
— em símbolos:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
— é definido por indução da seguinte forma:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\bot$
|
||
\end_inset
|
||
|
||
: Nunca
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\bot$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w\Vdash p$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $w\in V(p)$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\neg B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\nVdash B$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\wedge C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M},w\Vdash C$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\vee C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B$
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Formula $\mathbf{M},w\Vdash C$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv(B\rightarrow C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\nVdash B$
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Formula $\mathbf{M},w\Vdash C$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\square B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash B$
|
||
\end_inset
|
||
|
||
para todo
|
||
\begin_inset Formula $w'\in W$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\equiv\diamondsuit B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash B$
|
||
\end_inset
|
||
|
||
para pelo menos um
|
||
\begin_inset Formula $w'\in W$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Note que, de acordo com a cláusula 7, uma fórmula
|
||
\begin_inset Formula $\square B$
|
||
\end_inset
|
||
|
||
é verdadeira em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
, sempre que não há qualquer
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
.
|
||
Em um tal caso,
|
||
\begin_inset Formula $\square B$
|
||
\end_inset
|
||
|
||
é vacuamente verdadeiro em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
|
||
\begin_inset Formula $\square B$
|
||
\end_inset
|
||
|
||
também pode ser satisfeito em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
, mesmo se
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
não é.
|
||
A verdade de
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
não garante a verdade de
|
||
\begin_inset Formula $\diamondsuit B$
|
||
\end_inset
|
||
|
||
em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Isto vale, entretanto, se
|
||
\begin_inset Formula $Rww$
|
||
\end_inset
|
||
|
||
, ou seja, se
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
é reflexiva.
|
||
Se não há
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M},w\nVdash\diamondsuit A$
|
||
\end_inset
|
||
|
||
, para qualquer A.
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
1.
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
2.
|
||
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\diamondsuit A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\neg\square\neg A$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "proposicao1.7"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
1.
|
||
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w\nVdash\diamondsuit\neg A$
|
||
\end_inset
|
||
|
||
por meio da definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash$
|
||
\end_inset
|
||
|
||
.
|
||
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\diamondsuit\neg A$
|
||
\end_inset
|
||
|
||
sse para algum
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash\neg A$
|
||
\end_inset
|
||
|
||
.
|
||
Logo,
|
||
\begin_inset Formula $\mathbf{M},w\nVdash\diamondsuit\neg A$
|
||
\end_inset
|
||
|
||
sse para todo
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathbf{M},w'\nVdash\neg A$
|
||
\end_inset
|
||
|
||
.
|
||
Também temos que
|
||
\begin_inset Formula $\mathbf{M},w'\nVdash\neg A$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash A$
|
||
\end_inset
|
||
|
||
.
|
||
Juntando, temos que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\neg\diamondsuit\neg A$
|
||
\end_inset
|
||
|
||
sse para todo
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash A$
|
||
\end_inset
|
||
|
||
.
|
||
Novamente, pela definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash$
|
||
\end_inset
|
||
|
||
, isso é o casso sse
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
2.
|
||
Exercício
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Verdade em um modelo
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Às vezes é de interesse investigar quais fórmulas são verdadeiras em qualquer
|
||
mundo em uma dado modelo.
|
||
Introduziremos uma notação para isto.
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Uma fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeira em um modelo
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
, escrita
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
, se e somente se
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
para qualquer
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
1.
|
||
Se
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M}\nVdash\neg A$
|
||
\end_inset
|
||
|
||
, mas não vice-versa
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
2.
|
||
Se
|
||
\begin_inset Formula $\mathbf{M}\Vdash A\rightarrow B$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
somente se
|
||
\begin_inset Formula $\mathbf{M}\Vdash B$
|
||
\end_inset
|
||
|
||
, mas não vice-versa
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
1.
|
||
Se
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeiro em todos os mundos possíveis em
|
||
\begin_inset Formula $W$
|
||
\end_inset
|
||
|
||
e, uma vez que
|
||
\begin_inset Formula $W\neq\emptyset$
|
||
\end_inset
|
||
|
||
, não ser [o caso] que
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
, pois, caso contrário,
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
teria de ser verdadeiro e falso em algum mundo.
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Por outro lado, se
|
||
\begin_inset Formula $\mathbf{M}\nVdash\neg A$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeiro em algum mundo
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
.
|
||
Não se segue que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
,
|
||
\emph on
|
||
para qualquer
|
||
\emph default
|
||
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
.
|
||
Por exemplo, no modelo da Figura
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
ref{fig:simples}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathbf{M}\nVdash\neg p$
|
||
\end_inset
|
||
|
||
e também
|
||
\begin_inset Formula $\mathbf{M}\nVdash p$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
2.
|
||
Assuma que
|
||
\begin_inset Formula $\mathbf{M}\Vdash A\rightarrow B$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
; mostre que
|
||
\begin_inset Formula $\mathbf{M}\Vdash B$
|
||
\end_inset
|
||
|
||
.
|
||
Seja
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
um mundo arbitrário.
|
||
Então
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A\rightarrow B$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
, assim
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B$
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
era arbitrário,
|
||
\begin_inset Formula $\mathbf{M}\Vdash B$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Para mostrar que a inversa falha, precisamos encontrar um modelo
|
||
\begin_inset Formula $M$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
somente se
|
||
\begin_inset Formula $\mathbf{M}\Vdash B$
|
||
\end_inset
|
||
|
||
, mas
|
||
\begin_inset Formula $\mathbf{M}\nVdash A\rightarrow B$
|
||
\end_inset
|
||
|
||
.
|
||
Considere novamente o modelo da Figura
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
ref{fig:simples}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M}\nVdash p$
|
||
\end_inset
|
||
|
||
e, portanto, (vacuamente)
|
||
\begin_inset Formula $\mathbf{M}\Vdash p$
|
||
\end_inset
|
||
|
||
somente se
|
||
\begin_inset Formula $\mathbf{M}\Vdash q$
|
||
\end_inset
|
||
|
||
.
|
||
Entretanto,
|
||
\begin_inset Formula $\mathbf{M}\nVdash p\rightarrow q$
|
||
\end_inset
|
||
|
||
, pois
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é verdadeiro, mas
|
||
\begin_inset Formula $q$
|
||
\end_inset
|
||
|
||
é falso em
|
||
\begin_inset Formula $w_{1}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Validade
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Fórmulas que são verdadeiras em todos os modelos, isto é, verdadeiras em
|
||
qualquer mundo em qualquer modelo, são particularmente interessantes.
|
||
Elas representam aquelas proposições modais que são verdadeiras independentemen
|
||
te de como
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
são interpretados, contanto que a interpretação seja
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
normal
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
no sentido em que ela é gerada por alguma relação de acessibilidade sobre
|
||
mundos possíveis.
|
||
Chamamos tais fórmulas
|
||
\emph on
|
||
válidas
|
||
\emph default
|
||
.
|
||
Por exemplo,
|
||
\begin_inset Formula $\square(p\wedge q)\rightarrow\square p$
|
||
\end_inset
|
||
|
||
é válida.
|
||
Algumas fórmulas que esperaríamos como sendo válida em base da interpretação
|
||
alética de
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
não são, entretanto, válidas.
|
||
Parte do interesse de modelos relacionais é que interpretações diferentes
|
||
de
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
podem ser capturadas por diferentes tipos de relações de acessibilidade.
|
||
Isto sugere que deveríamos definir validade não apenas relativa a todos
|
||
|
||
\emph on
|
||
os modelos
|
||
\emph default
|
||
, mas também relativa a todos os modelos
|
||
\emph on
|
||
de um certo tipo
|
||
\emph default
|
||
.
|
||
Será visto, por exemplo, que [It will turn out, e.
|
||
g., that]
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
é verdadeira em todos os modelos em que qualquer mundo é acessível a partir
|
||
de si mesmo, ou seja, quando
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
é reflexiva.
|
||
Definir validade relativa a classes de modelos capacita-nos a formular
|
||
isto de forma sucinta:
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
é válida na classe de modelos reflexivos.
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Uma fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
|
||
\emph on
|
||
é válida
|
||
\emph default
|
||
em uma classe
|
||
\begin_inset Formula $\mathscr{C}$
|
||
\end_inset
|
||
|
||
de modelos, se ela é verdadeira em qualquer modelo em
|
||
\begin_inset Formula $\mathscr{C}$
|
||
\end_inset
|
||
|
||
(ou seja, verdadeira em qualquer mundo em qualquer modelo em
|
||
\begin_inset Formula $\mathscr{C}$
|
||
\end_inset
|
||
|
||
).
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é válida em
|
||
\begin_inset Formula $\mathscr{C}$
|
||
\end_inset
|
||
|
||
, escrevemos
|
||
\begin_inset Formula $\mathscr{C}\models A$
|
||
\end_inset
|
||
|
||
e escrevemos
|
||
\begin_inset Formula $\models A$
|
||
\end_inset
|
||
|
||
, se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é válido na classe de
|
||
\emph on
|
||
todos
|
||
\emph default
|
||
os modelos.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é válida em
|
||
\begin_inset Formula $\mathscr{C}$
|
||
\end_inset
|
||
|
||
, então ela é também válida em cada classe
|
||
\begin_inset Formula $\mathscr{C}'\subseteq\mathscr{C}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é válida, então
|
||
\begin_inset Formula $\square A$
|
||
\end_inset
|
||
|
||
é válida
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Assuma que
|
||
\begin_inset Formula $\models A$
|
||
\end_inset
|
||
|
||
.
|
||
Mostre que
|
||
\begin_inset Formula $\models\square A$
|
||
\end_inset
|
||
|
||
.
|
||
Seja
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
um modelo e
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
.
|
||
Se
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash A$
|
||
\end_inset
|
||
|
||
, uma vez que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é válida e, assim,
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash\square A$
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
são arbitrários, então
|
||
\begin_inset Formula $\models\square A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Instâncias tautológicas
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Uma fórmula modalmente livre [modal-free formula] se ela é verdadeira sob
|
||
qualquer atribuição de valor de verdade.
|
||
Claramente qualquer tautologia é verdadeira em qualquer mundo em qualquer
|
||
modelo.
|
||
Mas, para as fórmulas que envolvem
|
||
\begin_inset Formula $\square$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit$
|
||
\end_inset
|
||
|
||
, a noção de tautologia não é definida.
|
||
Por exemplo,
|
||
\begin_inset Formula $\square p\vee\neg\square p$
|
||
\end_inset
|
||
|
||
— uma instância do princípio do terceiro excluído — é válido? A noção de
|
||
|
||
\emph on
|
||
instância tautológica
|
||
\emph default
|
||
ajuda: uma fórmula que é uma instância de substituição de uma tautologia
|
||
(não modal).
|
||
Não é surpreendente, mas ainda requer prova, o fato de que qualquer instância
|
||
tautologia seja válida.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Uma fórmula
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
é uma instância tautológica se e somente se há uma tautologia modalmente
|
||
livre [modal-free tautology]
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
com variáveis proposicionais
|
||
\begin_inset Formula $p_{1},\ldots,p_{n}$
|
||
\end_inset
|
||
|
||
e fórmulas
|
||
\begin_inset Formula $D_{1},\ldots D_{n}$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $B\equiv A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Lemma
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "lema14"
|
||
|
||
\end_inset
|
||
|
||
Suponha que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
seja uma fórmula modalmente livre cujas variáveis proposicionais são
|
||
\begin_inset Formula $p_{1},\ldots,p_{n}$
|
||
\end_inset
|
||
|
||
e sejam
|
||
\begin_inset Formula $D_{1},\ldots,D_{n}$
|
||
\end_inset
|
||
|
||
fórmulas modais.
|
||
Então para qualquer atribuição
|
||
\begin_inset Formula $\mathcal{V}$
|
||
\end_inset
|
||
|
||
, qualquer modelo
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
e qualquer
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $\mathcal{V}(p_{i})=\mathrm{T}$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathbf{M},w\Vdash D_{i}$
|
||
\end_inset
|
||
|
||
, temos que
|
||
\begin_inset Formula $v\models A$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Por indução sobre
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
1.
|
||
|
||
\begin_inset Formula $A\equiv\bot$
|
||
\end_inset
|
||
|
||
: Tanto
|
||
\begin_inset Formula $\mathcal{V}\nvDash\bot$
|
||
\end_inset
|
||
|
||
como
|
||
\begin_inset Formula $\mathbf{M},w\models\bot$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
2.
|
||
|
||
\begin_inset Formula $A\equiv p_{i}$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="3" columns="4">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models p_{i}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}(p_{i})=\mathrm{T}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathcal{V}\models p_{i}$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash D_{i}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela hipótese;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash p_{i}[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pois
|
||
\begin_inset Formula $p_{i}[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
3.
|
||
|
||
\begin_inset Formula $A\equiv\neg B$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="3" columns="4">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models\neg B$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\nvDash\mathrm{B}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathcal{V}\models$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\nVdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela hipótese indutiva;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\neg B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela def.
|
||
de
|
||
\begin_inset Formula $\mathcal{V}\models$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
4.
|
||
|
||
\begin_inset Formula $A\equiv(B\wedge C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="4" columns="4">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models B\wedge C$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models B$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathcal{V}\models C$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathcal{V}\models$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
e
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela hipótese indutiva;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash(B\wedge C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
5.
|
||
|
||
\begin_inset Formula $A\equiv(B\vee C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="4" columns="4">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models B\vee C$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models B$
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Formula $\mathcal{V}\models C$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathcal{V}\models$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
ou
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela hipótese indutiva;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash(B\vee C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
6.
|
||
|
||
\begin_inset Formula $A\equiv(B\rightarrow C)$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
|
||
\backslash
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="4" columns="4">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="center" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\models B\rightarrow C$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathcal{V}\nvDash B$
|
||
\end_inset
|
||
|
||
ou
|
||
\begin_inset Formula $\mathcal{V}\models C$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathcal{V}\models$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\nVdash B[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
ou
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash C[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela hipótese indutiva;
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\Longleftrightarrow$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\mathbf{M},w\Vdash(B\rightarrow C)[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="center" valignment="top" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
pela definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
Todas as instâncias tautológicas são válidas
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Vamos prova a contrapositiva.
|
||
Suponha que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é tal que
|
||
\begin_inset Formula $\mathbf{M},w\nVdash A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
para algum modelo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
e algum mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Defina uma atribuição
|
||
\begin_inset Formula $\mathcal{V}$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $\mathcal{V}(p_{i})=\mathrm{T}$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathbf{M},w\Vdash D_{i}$
|
||
\end_inset
|
||
|
||
(e
|
||
\begin_inset Formula $\mathcal{V}$
|
||
\end_inset
|
||
|
||
atribui valores arbitrários a
|
||
\begin_inset Formula $q\notin\{p_{1},\ldots,p_{n}\}$
|
||
\end_inset
|
||
|
||
).
|
||
Então pelo Lema
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "lema14"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathcal{V}\nvDash A$
|
||
\end_inset
|
||
|
||
e, assim,
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
não é tautologia.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Esquemas e validade
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Um esquema é um conjunto de fórmulas que inclui todas e somente [
|
||
\emph on
|
||
all and only
|
||
\emph default
|
||
] as instâncias de substituição de alguma fórmula modal
|
||
\begin_inset Formula $C$
|
||
\end_inset
|
||
|
||
, ou seja,
|
||
\begin_inset Formula $\{B:\exists D_{1},\ldots,\exists D_{n}(B=C[D_{1}/p_{1},\ldots,D_{n}/p_{n}])\}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Definition
|
||
A fórmula
|
||
\begin_inset Formula $C$
|
||
\end_inset
|
||
|
||
é chamada a fórmula característica [
|
||
\emph on
|
||
characteristic formula
|
||
\emph default
|
||
] do esquema e ela é única até [up to]
|
||
\begin_inset Note Note
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
Ver melhor esse termo.
|
||
Em geral é usado em contexto de mesmidade de estrutura
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
a renomeação das variáveis proposicionais.
|
||
Uma fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é uma instância de um esquema, se ela é um membro do conjunto.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
É conveniente denotar um esquema por meio de expressão metalinguística obtida
|
||
por de meio da substituição dos componentes atômicos de
|
||
\begin_inset Formula $C$
|
||
\end_inset
|
||
|
||
por `
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
', `
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
',
|
||
\begin_inset Formula $\ldots$
|
||
\end_inset
|
||
|
||
.Assim, por exemplo, os seguintes denotam esquemas: `
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
', `
|
||
\begin_inset Formula $A\rightarrow\square A$
|
||
\end_inset
|
||
|
||
', `
|
||
\begin_inset Formula $A\rightarrow(B\rightarrow A)$
|
||
\end_inset
|
||
|
||
'.
|
||
Eles correspondem às fórmulas características
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $p\rightarrow\square p$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $p\rightarrow(q\rightarrow p)$
|
||
\end_inset
|
||
|
||
.
|
||
O esquema `
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
' denota o conjunto de
|
||
\emph on
|
||
todas
|
||
\emph default
|
||
as fórmulas.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Um esquema será
|
||
\emph on
|
||
verdadeiro
|
||
\emph default
|
||
em um modelo se e somente se todas as suas instâncias forem verdadeiras
|
||
no modelo; e um esquema será válido se e somente se ele for verdadeiro
|
||
em qualquer modelo.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
O seguinte esquema K é válido:
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
begin{equation}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
square(A
|
||
\backslash
|
||
rightarrow B)
|
||
\backslash
|
||
rightarrow(
|
||
\backslash
|
||
square A
|
||
\backslash
|
||
rightarrow
|
||
\backslash
|
||
square B)
|
||
\backslash
|
||
tag{K}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
end{equation}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Precisamos mostrar que todas as instâncias do esquema são verdadeiras em
|
||
qualquer mundo em qualquer modelo.
|
||
Assim, sejam
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
arbitrários.
|
||
Para mostrar que um condicional é verdadeiro em um mundo, assumimos que
|
||
o antecedente é verdadeiro para mostrar que o consequente é verdadeiro
|
||
também, Neste caso, assuma que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square(A\rightarrow B)$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square A$
|
||
\end_inset
|
||
|
||
.
|
||
Precisamos mostrar que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square B$
|
||
\end_inset
|
||
|
||
.
|
||
Assim, seja
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
arbitrário tal que
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
.
|
||
Então, pela primeira suposição, temos que
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash A\rightarrow B$
|
||
\end_inset
|
||
|
||
e, pela segunda suposição, temos que
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash A$
|
||
\end_inset
|
||
|
||
.
|
||
Logo, segue-se que
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash B$
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
era arbitrário, temos que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square B$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
O seguinte esquema DUAL
|
||
\emph on
|
||
é válido
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "proposicao1.19"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
begin{equation}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
diamondsuit A
|
||
\backslash
|
||
leftrightarrow
|
||
\backslash
|
||
neg
|
||
\backslash
|
||
square
|
||
\backslash
|
||
neg A
|
||
\backslash
|
||
tag{DUAL}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
end{equation}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Exercício
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
Se
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $A\rightarrow B$
|
||
\end_inset
|
||
|
||
são verdadeiras em um mundo, em um modelo, então
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
também é.
|
||
Assim, as fórmulas válidas são fechadas sob modus ponens.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
Uma fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
será válida sse todas as suas instâncias de substituição forem também.
|
||
Em outras palavras, um esquema é válido sse sua fórmula característica
|
||
também for.
|
||
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "proposicao1.21"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
A direção
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
se
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
é óbvia, uma vez que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é uma instância de substituição de si mesma.
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Para provar a direção
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
somente se
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
, mostramos o seguinte: suponha que
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
é um modelo modal e que
|
||
\begin_inset Formula $B\equiv A[D_{1}/p_{1},\ldots,D_{n}/p_{n}]$
|
||
\end_inset
|
||
|
||
é uma instância de substituição de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
.
|
||
Defina
|
||
\begin_inset Formula $\mathbf{M'}=<W,R,V'>$
|
||
\end_inset
|
||
|
||
por meio de
|
||
\begin_inset Formula $V'(p_{i})=\{w:\mathbf{M}\Vdash D_{i}w\}$
|
||
\end_inset
|
||
|
||
.
|
||
Então
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B$
|
||
\end_inset
|
||
|
||
sse
|
||
\begin_inset Formula $\mathbf{M'},w\Vdash A$
|
||
\end_inset
|
||
|
||
, para qualquer
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
(a prova será deixada como exercício).
|
||
Suponha agora que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
era válida, mas alguma instância de substituição
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
de A não era válida.
|
||
Então, para algum
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
e algum
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathbf{M},w\nVdash B$
|
||
\end_inset
|
||
|
||
.
|
||
Mas, então,
|
||
\begin_inset Formula $\mathbf{M'},w\nVdash A$
|
||
\end_inset
|
||
|
||
pela reivindicação e
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
não é válida, uma contradição.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Note, entretanto, que não é verdadeiro que um esquema seja verdadeiro em
|
||
um modelo sse sua fórmula característica também é.
|
||
Obviamente, a direção
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
somente se
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
vale: se qualquer instância de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
, então a própria
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
.
|
||
Contudo, pode acontecer que
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
seja verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
, mas alguma instância de
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
seja falsa em algum mundo em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
.
|
||
Para um contraexemplo muito simples, considere
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
em um modelo com apenas um mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $V(p)=\{w\}$
|
||
\end_inset
|
||
|
||
, de forma que
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é verdadeiro em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Mas
|
||
\begin_inset Formula $\bot$
|
||
\end_inset
|
||
|
||
é uma instância de
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
e não é verdadeiro em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\align center
|
||
\begin_inset Float table
|
||
wide false
|
||
sideways false
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
\align center
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="7" columns="2">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
Esquemas válidos
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
Esquemas inválidos
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square(A\rightarrow B)\rightarrow(\diamondsuit A\rightarrow\diamondsuit B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square(A\vee B)\rightarrow(\square A\vee\square B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\diamondsuit(A\rightarrow B)\rightarrow(\square A\rightarrow\diamondsuit B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $(\diamondsuit A\vee\diamondsuit B)\rightarrow\diamondsuit(A\wedge B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square(A\wedge B)\leftrightarrow(\square A\wedge\square B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $A\rightarrow\square A$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square A\rightarrow\square(B\rightarrow A)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square\diamondsuit A\rightarrow B$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\neg\diamondsuit A\rightarrow\square(A\rightarrow B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square\square A\rightarrow\square A$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" bottomline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\diamondsuit(A\vee B)\leftrightarrow(\diamondsuit A\vee\diamondsuit B)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" bottomline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square\diamondsuit A\rightarrow\diamondsuit\square A$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Caption Standard
|
||
|
||
\begin_layout Plain Layout
|
||
Esquemas válidos e (ou?) inválidos
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "tabela1.1"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Acarretamento [
|
||
\emph on
|
||
entailment
|
||
\emph default
|
||
]
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Com a definição de verdade em um mundo, podemos definir a relação de acarretamen
|
||
to entre fórmulas.
|
||
Uma fórmula
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
acarreta
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
sse sempre que
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
é verdadeira,
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeira também.
|
||
Aqui,
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
sempre que
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
significa
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
qualquer que seja o modelo que consideramos
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
assim como
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
qualquer que seja o mundo neste modelo que consideramos
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Box Boxed
|
||
position "t"
|
||
hor_pos "c"
|
||
has_inner_box 1
|
||
inner_pos "t"
|
||
use_parbox 0
|
||
use_makebox 0
|
||
width "100col%"
|
||
special "none"
|
||
height "1in"
|
||
height_special "totalheight"
|
||
thickness "0.1cm"
|
||
separation "3pt"
|
||
shadowsize "4pt"
|
||
framecolor "magenta"
|
||
backgroundcolor "white"
|
||
status open
|
||
|
||
\begin_layout Definition
|
||
Se
|
||
\begin_inset Formula $\varGamma$
|
||
\end_inset
|
||
|
||
é um conjunto de fórmulas e
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é uma fórmula, então
|
||
\begin_inset Formula $\varGamma$
|
||
\end_inset
|
||
|
||
acareta
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
— em símbolos:
|
||
\begin_inset Formula $\varGamma\models A$
|
||
\end_inset
|
||
|
||
— se e somente se para qualquer modelo
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
e qualquer mundo
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
, se
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B$
|
||
\end_inset
|
||
|
||
para qualquer
|
||
\begin_inset Formula $B\in\varGamma$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
.
|
||
Se
|
||
\begin_inset Formula $\varGamma$
|
||
\end_inset
|
||
|
||
contém uma única fórmula
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
, escrevemos
|
||
\begin_inset Formula $B\models A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset VSpace 8pt
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Example
|
||
Para mostrar que uma fórmula acarreta uma outra, temos de raciocionar sobre
|
||
todos os modelos, usando a definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash$
|
||
\end_inset
|
||
|
||
.
|
||
Por exemplo, para mostrar que
|
||
\begin_inset Formula $p\rightarrow\diamondsuit p\models\square\neg p\rightarrow\neg p$
|
||
\end_inset
|
||
|
||
, poderíamos argumentae como se segue: considere um modelo
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
e suponha que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
.
|
||
Temos de mostrar que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square\neg p\rightarrow\neg p$
|
||
\end_inset
|
||
|
||
.
|
||
Suponha que isso não é o caso.
|
||
Então
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square\neg p$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M},w\nVdash\neg p$
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que
|
||
\begin_inset Formula $\mathbf{M},w\nVdash\neg p$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M},w\Vdash p$
|
||
\end_inset
|
||
|
||
.
|
||
Pela suposição,
|
||
\begin_inset Formula $\mathbf{M},w\Vdash p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
, assim
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\diamondsuit p$
|
||
\end_inset
|
||
|
||
.
|
||
Pela definição de
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\diamondsuit p$
|
||
\end_inset
|
||
|
||
, há um
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash p$
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square\neg p$
|
||
\end_inset
|
||
|
||
, temos que
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash\neg p$
|
||
\end_inset
|
||
|
||
, uma contradição.
|
||
\end_layout
|
||
|
||
\begin_layout Example
|
||
Para mostrar que uma fórmula
|
||
\begin_inset Formula $B$
|
||
\end_inset
|
||
|
||
não implica uma outra
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
, temos de dar um contraexemplo, ou seja, um modelo
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
em que mostramos que em algum mundo
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $\mathbf{M},w\Vdash B$
|
||
\end_inset
|
||
|
||
, mas
|
||
\begin_inset Formula $\mathbf{M},w\nVdash A$
|
||
\end_inset
|
||
|
||
.
|
||
Considere o modelo na Figura
|
||
\begin_inset CommandInset ref
|
||
LatexCommand formatted
|
||
reference "figura2"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
.
|
||
Temos que
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash\diamondsuit p$
|
||
\end_inset
|
||
|
||
e, assim,
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
.
|
||
Entretanto, uma vez que
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash\square p$
|
||
\end_inset
|
||
|
||
, mas
|
||
\begin_inset Formula $\mathbf{M},w_{1}\nVdash p$
|
||
\end_inset
|
||
|
||
, temos que
|
||
\begin_inset Formula $\mathbf{M},w_{1}\nVdash\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Example
|
||
Frequentemente exemplos bastante simples são suficientes.
|
||
O modelo
|
||
\begin_inset Formula $\mathbf{M'}=\{W',R',V'\}$
|
||
\end_inset
|
||
|
||
com
|
||
\begin_inset Formula $W'=\{w\}$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $R'=\emptyset$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $V(p)=\emptyset$
|
||
\end_inset
|
||
|
||
é também um contraexemplo: uma vez que
|
||
\begin_inset Formula $\mathbf{M'},w\nVdash p$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $\mathbf{M'},w\Vdash p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
.
|
||
Como nenhum mundo é acessível a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
, temos que
|
||
\begin_inset Formula $\mathbf{M'},w\Vdash\square p$
|
||
\end_inset
|
||
|
||
e, assim, que
|
||
\begin_inset Formula $\mathbf{M'},w\nVdash\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Float figure
|
||
wide false
|
||
sideways false
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
\align center
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psscalebox{.7 .7} % Change this value to rescale the drawing.
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
{
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
begin{pspicture}(0,-3.6)(10.17,3.6)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](1.2,2.4){1.2}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](8.4,2.4){1.2}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.8,-2.4){1.2}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.8,2.4){$w_2$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](8.0,2.4){$w_3$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](4.4,-2.8){$w_1$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](2.8,2.4){$p$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](10.0,2.4){$p$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](6.4,-2.4){$
|
||
\backslash
|
||
neg p$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(3.6,-1.2)(2.0,1.2)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(6.0,-1.2)(8.0,1.2)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
end{pspicture}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Caption Standard
|
||
|
||
\begin_layout Plain Layout
|
||
Contraexemplo para
|
||
\begin_inset Formula $p\rightarrow\diamondsuit p\models\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "figura2"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Problema
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
|
||
\series bold
|
||
Problema 1.1
|
||
\series default
|
||
Considere o modelo da Figura
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
ref{fig:simples}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
.
|
||
Quais das seguintes afirmações valem?
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash q$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{3}\Vdash\neg q$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash p\vee q$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash\square(p\vee q)$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{3}\Vdash\square q$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{3}\Vdash\square\bot$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash\lozenge q$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash\square q$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash\neg\square\square\neg q$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
|
||
\series bold
|
||
Problema 1.2
|
||
\series default
|
||
Complete a prova da Proposição
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "proposicao1.7"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Problema 1.3
|
||
\series default
|
||
Seja
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
um modelo e suponha que
|
||
\begin_inset Formula $w_{1},w_{2}\in W$
|
||
\end_inset
|
||
|
||
são tais que:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $w_{1}\in V(p)$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $w_{2}\in V(p)$
|
||
\end_inset
|
||
|
||
; e
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
para todo
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
,
|
||
\begin_inset Formula $Ew_{1}w$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $Rw_{2}w$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Usando indução sobre fórmulas, mostre que para qualquer fórmula
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},w_{1}\Vdash A$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathbf{M},w_{2}\Vdash A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Problema 1.4
|
||
\series default
|
||
Seja
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
.
|
||
Mostre que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\neg\diamondsuit A$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square\neg A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Problema 1.5
|
||
\series default
|
||
Considere o seguinte modelo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
para a linguagem que contém
|
||
\begin_inset Formula $p_{1},p_{2},p_{3}$
|
||
\end_inset
|
||
|
||
como as únicas variáveis proposicionais:
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\align center
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psscalebox{.7 .7} % Change this value to rescale the drawing.
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
{
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
begin{pspicture}(0,-4.630786)(12.22,4.630786)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](2.24,1.6492139){1.46}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](10.1,1.709214){1.46}
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](6.1,-3.1707861){1.46}
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](1.92,1.5092139){$w_1$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](10.0,1.549214){$w_3$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](5.96,-3.350786){$w_2$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.26,1.989214){$p_1$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.04,1.549214){$
|
||
\backslash
|
||
neg p_2$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.0,1.109214){$
|
||
\backslash
|
||
neg p_3$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](11.92,2.009214){$p_1$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](11.92,1.5092139){$p_2$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](11.92,1.0092139){$p_3$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](8.14,-2.790786){$p_1$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](8.14,-3.290786){$p_2$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](7.96,-3.730786){$
|
||
\backslash
|
||
neg p_3$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(7.2,-1.890786)(9.08,0.36921397)
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(2.94,0.12921396)(4.7,-2.090786)
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(3.8,1.789214)(8.4,1.789214)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput{-43.384533}(0.06654787,7.865721){
|
||
\backslash
|
||
psarc[linecolor=black, linewidth=0.04, dimen=outer, arrowsize=0.05291667cm
|
||
2.0,arrowlength=1.4,arrowinset=0.0]{<-}(9.92,3.8492138){0.68}{0.0}{270.0}}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
end{pspicture}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
As seguinte fórmulas e esquemas são verdadeiras no modelo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
, ou seja, verdadeiras em qualquer mundo em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
? Explique.
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
atômica);
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $A\rightarrow\diamondsuit A$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
arbitrária);
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
atômica);
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\neg p\rightarrow\lozenge\square p$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
atômica);
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\diamondsuit\square A$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
arbitrária);
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\diamondsuit\square p$
|
||
\end_inset
|
||
|
||
(para
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
atômica).
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
|
||
\series bold
|
||
Problema 1.7
|
||
\series default
|
||
Mostre que
|
||
\begin_inset Formula $A\rightarrow\square A$
|
||
\end_inset
|
||
|
||
é valida na classe
|
||
\begin_inset Formula $\mathscr{C}$
|
||
\end_inset
|
||
|
||
de modelos
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
, em que
|
||
\begin_inset Formula $W=\{w\}$
|
||
\end_inset
|
||
|
||
.
|
||
Similarmente mostre que
|
||
\begin_inset Formula $B\rightarrow\square A$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\diamondsuit A\rightarrow B$
|
||
\end_inset
|
||
|
||
são válidas na classe de modelos
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
, em que
|
||
\begin_inset Formula $R=\emptyset$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Problema 1.8
|
||
\series default
|
||
Prove a Proposição
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "proposicao1.19"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Proposição 1.9
|
||
\series default
|
||
Prove a reivindicação na parte
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
somente se
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
da prova da Proposição
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "proposicao1.21"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
(dica: use indução sobre
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
).
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Proposição 1.10
|
||
\series default
|
||
Mostre que nenhuma das seguintes fórmulas são válidas:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Argument item:1
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
D:
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\square p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Argument item:1
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
T:
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Argument item:1
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
B:
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $p\rightarrow\square\diamondsuit p$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Argument item:1
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
4:
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\square p\rightarrow\square\square p$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Argument item:1
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
5:
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $\diamondsuit p\rightarrow\square\diamondsuit p$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
|
||
\series bold
|
||
Problema 1.11
|
||
\series default
|
||
Prove que os esquemas na primeira coluna da tabela
|
||
\begin_inset CommandInset ref
|
||
LatexCommand formatted
|
||
reference "tabela1.1"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
são válidos e os das segunda coluna são inválidos.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Problema 1.12
|
||
\series default
|
||
Decida se os seguintes esquemas são válidos ou inválidos:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $(\diamondsuit A\rightarrow\square B)\rightarrow(\square A\rightarrow\square B)$
|
||
\end_inset
|
||
|
||
;
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\diamondsuit(A\rightarrow B)\vee\square(B\rightarrow A)$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
|
||
\series bold
|
||
Problema 1.13
|
||
\series default
|
||
Para cada um dos seguintes esquemas, encontre um modelo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
tal que qualquer instância da fórmula é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
:
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $p\rightarrow\diamondsuit\diamondsuit p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Enumerate
|
||
\begin_inset Formula $\diamondsuit p\rightarrow\square p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
|
||
\series bold
|
||
Problema 1.14
|
||
\series default
|
||
Mostre que
|
||
\begin_inset Formula $\square(A\wedge B)\models\square A$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\noindent
|
||
|
||
\series bold
|
||
Problema 1.15
|
||
\series default
|
||
Mostre que
|
||
\begin_inset Formula $\square(p\rightarrow q)\nvDash p\rightarrow\square q$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $p\rightarrow\square q\nvDash\square(p\rightarrow q)$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Chapter
|
||
Definabilidade de estrutura [Frame definability]
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Introdução
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Uma questão que interessa aos lógicos modais é a conexão entre a relação
|
||
de acessibilidade e a verdade de certas fórmulas nos modelos com esta relação
|
||
de acessibilidade.
|
||
Por exemplo, suponha que a relação de acessibilidade é reflexiva, ou seja,
|
||
para qualquer
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
, Rww.
|
||
Em outros palavras, qualquer mundo é acessível a partir de si mesmo.
|
||
Isto significa que quando
|
||
\begin_inset Formula $\square A$
|
||
\end_inset
|
||
|
||
é verdadeiro em um mundo w, o próprio w está entre os mundos acessíveis
|
||
em que A deve ser, portanto, verdadeiro.
|
||
Assim, se a relação de acessibilidade R de
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
é reflexiva, então quaisquer que sejam o mundo w e a fórmula A que tomamos,
|
||
|
||
\begin_inset Formula $\square A\rightarrow A$
|
||
\end_inset
|
||
|
||
será verdadeiro no modelo (em outra palavras, o esquema
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
e todas as instâncias de substituição dele são verdadeiras em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
).
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A inversa, entretanto, é falsa.
|
||
Por exemplo, não é o caso que se
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
é reflexiva.
|
||
Pois podemos encontrar facilmente um modelo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
não-reflexivo em que
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
é verdadeira em todos os mundos: tome o modelo com um único mudo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
, que não é acessível a partir de si mesmo, mas com
|
||
\begin_inset Formula $w\in V(p)$
|
||
\end_inset
|
||
|
||
.
|
||
Selecionando o valor de verdade de
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
adequadamente, podemos fazer
|
||
\begin_inset Formula $\square A\rightarrow A$
|
||
\end_inset
|
||
|
||
verdadeira em um modelo que não é reflexivo.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
A solução é remover a atribuição de variável
|
||
\begin_inset Formula $V$
|
||
\end_inset
|
||
|
||
da equação.
|
||
Se exigirmos que
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
é verdadeira em todos os mundos em
|
||
\begin_inset Formula $W$
|
||
\end_inset
|
||
|
||
, independentemente de quais mundos estão em
|
||
\begin_inset Formula $V(p)$
|
||
\end_inset
|
||
|
||
, então é necessário que
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
seja reflexiva.
|
||
Pois, em qualquer modelo não-reflexivo, haverá pelo menos um mundo
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
tal que não é o caso que
|
||
\begin_inset Formula $Rww$
|
||
\end_inset
|
||
|
||
.
|
||
Se estabelecermos
|
||
\begin_inset Formula $V(p)=W\backslash\{w\}$
|
||
\end_inset
|
||
|
||
, então
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
será verdadeira em todos os mundos, exceto em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
e, assim, será verdadeira em todos os mundos acessíveis a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
(uma vez que é garantido que
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
não é acessível a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
é o único mundo em que
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é falsa).
|
||
Por outro lado,
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
é falsa em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
e, assim,
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
é falsa em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Isto sugere que deveríamos introduzir uma notação para estruturas de modelo
|
||
sem uma valoração: chamamo-las
|
||
\emph on
|
||
frames
|
||
\emph default
|
||
.
|
||
Um
|
||
\emph on
|
||
frame
|
||
\emph default
|
||
|
||
\begin_inset Formula $\mathcal{F}$
|
||
\end_inset
|
||
|
||
é simplesmente um par
|
||
\begin_inset Formula $<W,R>$
|
||
\end_inset
|
||
|
||
que consiste em um conjunto de mundos com uma relação de acessibilidade.
|
||
Qualquer modelo
|
||
\begin_inset Formula $<W,R,V>$
|
||
\end_inset
|
||
|
||
é, então, como dizemos, baseado no
|
||
\emph on
|
||
frame
|
||
\emph default
|
||
|
||
\begin_inset Formula $<W,R>$
|
||
\end_inset
|
||
|
||
.
|
||
Inversamente, um
|
||
\emph on
|
||
frame
|
||
\emph default
|
||
determina a classe de modelos baseados nele; e uma classe de
|
||
\emph on
|
||
frames
|
||
\emph default
|
||
determina a classe de modelos que são baseados em qualquer
|
||
\emph on
|
||
frame
|
||
\emph default
|
||
na classe.
|
||
E podemos definir
|
||
\begin_inset Formula $\mathcal{F}\models A$
|
||
\end_inset
|
||
|
||
, a noção de uma fórmula ser
|
||
\emph on
|
||
válida
|
||
\emph default
|
||
em um
|
||
\emph on
|
||
frame
|
||
\emph default
|
||
como:
|
||
\begin_inset Formula $\mathbf{M}\Vdash A$
|
||
\end_inset
|
||
|
||
para todo
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
baseado em
|
||
\begin_inset Formula $\mathcal{F}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Com esta notação, podemos estabelecer relações de correspondência entre
|
||
fórmulas e classes de
|
||
\emph on
|
||
frames
|
||
\emph default
|
||
: por exemplo,
|
||
\begin_inset Formula $\mathcal{F}\models\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathcal{F}$
|
||
\end_inset
|
||
|
||
é reflexivo.
|
||
\end_layout
|
||
|
||
\begin_layout Section
|
||
Propriedades de relações de acessibilidade
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Algumas fórmulas modais são resultantes de características de propriedades
|
||
simples, e até mesmo comuns, da relação de acessibilidade.
|
||
Por um lado, isto significa que qualquer modelo que tem uma dada propriedade
|
||
faz a fórmula correspondente (e todas as instâncias de substituição dela)
|
||
verdadeira.
|
||
Começamos com cinco exemplos clássicos de tipos de relações de acessibilidade
|
||
e fórmulas cuja verdade eles garantem.
|
||
\end_layout
|
||
|
||
\begin_layout Theorem
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "Teorema2-1"
|
||
|
||
\end_inset
|
||
|
||
Seja
|
||
\begin_inset Formula $M=<W,R,V>$
|
||
\end_inset
|
||
|
||
um modelo.
|
||
Se
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
tem a propriedade à esquerda da tabela
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "tabela2-1"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
, qualquer instância da fórmula à direita é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Aqui é o caso para B: para mostrar que o esquema é verdadeiro em um modelo,
|
||
precisamos mostrar que todas as instâncias do esquema são verdadeiras em
|
||
todos os mundos no modelo.
|
||
Assim, seja
|
||
\begin_inset Formula $A\rightarrow\diamondsuit\square A$
|
||
\end_inset
|
||
|
||
uma dada instância de B e seja
|
||
\begin_inset Formula $w\in W$
|
||
\end_inset
|
||
|
||
um mundo arbitrário.
|
||
Suponha que o antecedente
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
é verdadeiro em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
, a fim de mostrar que
|
||
\begin_inset Formula $\square\diamondsuit A$
|
||
\end_inset
|
||
|
||
é verdadeira em
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Assim, precisamos mostrar que
|
||
\begin_inset Formula $\diamondsuit A$
|
||
\end_inset
|
||
|
||
é verdadeira em todos os mundos
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
acessíveis a partir de
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
.
|
||
Ora, para qualquer
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
tal que
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
, temos também, usando a hipótese da simetria, que
|
||
\begin_inset Formula $Rw'w$
|
||
\end_inset
|
||
|
||
(veja a Figura
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "figura2-1"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
).
|
||
Uma vez que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash A$
|
||
\end_inset
|
||
|
||
, temos que
|
||
\begin_inset Formula $\mathbf{M},w'\Vdash\diamondsuit A$
|
||
\end_inset
|
||
|
||
.
|
||
Uma vez que
|
||
\begin_inset Formula $w'$
|
||
\end_inset
|
||
|
||
era um mundo arbitrário tal que
|
||
\begin_inset Formula $Rww'$
|
||
\end_inset
|
||
|
||
, temos que
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square\diamondsuit A$
|
||
\end_inset
|
||
|
||
.
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Proof
|
||
Deixamos os outros casos como exercício.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Float table
|
||
wide false
|
||
sideways false
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
\align center
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="6" columns="2">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="left" valignment="top">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\emph on
|
||
Se R é ...
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
então ...
|
||
é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
serial:
|
||
\begin_inset Formula $\forall u\exists vRuv$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square p\rightarrow\diamondsuit p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset space \hfill{}
|
||
\end_inset
|
||
|
||
(D)
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
reflexiva:
|
||
\begin_inset Formula $\forall wRww$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square p\rightarrow p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset space \hfill{}
|
||
\end_inset
|
||
|
||
(T)
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
simetria:
|
||
\begin_inset Formula $\forall u\forall v(Ruv\rightarrow Rvu)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $p\rightarrow\square\diamondsuit p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset space \hfill{}
|
||
\end_inset
|
||
|
||
(B)
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
transitiva:
|
||
\begin_inset Formula $\forall u\forall v\forall w(Ruv\wedge Rvw\rightarrow Ruw)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square p\rightarrow\square\square p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset space \hfill{}
|
||
\end_inset
|
||
|
||
(4)
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
euclidiana:
|
||
\begin_inset Formula $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow Ruv)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\diamondsuit p\rightarrow\square\diamondsuit p$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset space \hfill{}
|
||
\end_inset
|
||
|
||
(5)
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Caption Standard
|
||
|
||
\begin_layout Plain Layout
|
||
Cinco fatos de correspondência
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "tabela2-1"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Float figure
|
||
wide false
|
||
sideways false
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
\align center
|
||
\begin_inset ERT
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psscalebox{.7 .7} % Change this value to rescale the drawing.
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
{
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
begin{pspicture}(0,-1.18)(5.18,1.18)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](0.63,0.53){0.63}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.46,0.44){$w$}
|
||
\backslash
|
||
rput[bl](4.42,0.46){$w'$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(1.38,1.16)(3.82,1.14)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
psline[linecolor=black, linewidth=0.04, arrowsize=0.05291667cm 2.0,arrowlength=1.4,a
|
||
rrowinset=0.0]{->}(3.7,0.02)(1.4,0.0)
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.04,-0.68){$
|
||
\backslash
|
||
Vdash A$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](0.04,-1.18){$
|
||
\backslash
|
||
Vdash
|
||
\backslash
|
||
square
|
||
\backslash
|
||
diamondsuit A$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
rput[bl](4.16,-0.62){$
|
||
\backslash
|
||
Vdash
|
||
\backslash
|
||
diamondsuit A$}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
pscircle[linecolor=black, linewidth=0.04, dimen=outer](4.55,0.55){0.63}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
|
||
\backslash
|
||
end{pspicture}
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
}
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Caption Standard
|
||
|
||
\begin_layout Plain Layout
|
||
O argumento a partir da simetria
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "figura2-1"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Note que as implicações inversas do Teorema
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "Teorema2-1"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
não valem: não é verdade que se um modelo verifica um esquema, então a
|
||
relação de acessibilidade deste modelo tem a propriedade correspondente.
|
||
No caso de T e modelos reflexivos, é fácil dar um contraexemplo de um modelo
|
||
no qual o próprio T falha: Sejam
|
||
\begin_inset Formula $W=\{w\}$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $V(p)=\emptyset$
|
||
\end_inset
|
||
|
||
.
|
||
Então
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
não é reflexivo, mas
|
||
\begin_inset Formula $\mathbf{M},w\Vdash\square p$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M},w\nVdash p$
|
||
\end_inset
|
||
|
||
.
|
||
Mas, aqui, temos justamente uma única instância de T que falha em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
, outras instâncias, por exemplo,
|
||
\begin_inset Formula $\square\neg p\rightarrow\neg p$
|
||
\end_inset
|
||
|
||
, são verdadeiras.
|
||
É mais difícil dar exemplos em que qualquer instância de substituição de
|
||
T é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
não é reflexiva.
|
||
Mas há também tais modelos:
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
Seja
|
||
\begin_inset Formula $\mathbf{M}=<W,R,V>$
|
||
\end_inset
|
||
|
||
um modelo tal que
|
||
\begin_inset Formula $W=\{u,v\}$
|
||
\end_inset
|
||
|
||
, em que os mundos
|
||
\begin_inset Formula $u$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $v$
|
||
\end_inset
|
||
|
||
estão relacionados pela R: ou seja, tanto
|
||
\begin_inset Formula $Ruv$
|
||
\end_inset
|
||
|
||
como
|
||
\begin_inset Formula $Rvu$
|
||
\end_inset
|
||
|
||
.
|
||
Suponha que para todo
|
||
\begin_inset Formula $p$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $u\in V(p)\Leftrightarrow v\in V(p)$
|
||
\end_inset
|
||
|
||
.
|
||
Então:
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
1.
|
||
Para todo
|
||
\begin_inset Formula $A$
|
||
\end_inset
|
||
|
||
:
|
||
\begin_inset Formula $\mathbf{M},u\Vdash A$
|
||
\end_inset
|
||
|
||
se e somente se
|
||
\begin_inset Formula $\mathbf{M},v\Vdash A$
|
||
\end_inset
|
||
|
||
(use indução sobre A).
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
2.
|
||
Qualquer instância de T é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Proposition
|
||
\noindent
|
||
Uma vez que
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
não é reflexiva (de fato, é irreflexiva), a inversa do Teorema
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "Teorema2-1"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
falha no caso de T (argumentos similares podem ser dados para alguns —
|
||
embora não todos — dos outros esquemas mencionados no Teorema
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "Teorema2-1"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Separator plain
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
Embora nosso foco será nas cinco fórmulas clássicas D, T, B, 4 e 5, registramos
|
||
na tabela
|
||
\begin_inset CommandInset ref
|
||
LatexCommand ref
|
||
reference "tabela2-2"
|
||
plural "false"
|
||
caps "false"
|
||
noprefix "false"
|
||
|
||
\end_inset
|
||
|
||
mais algumas propriedades de relações de acessibilidade.
|
||
A relação de acessibilidade
|
||
\begin_inset Formula $R$
|
||
\end_inset
|
||
|
||
é parcialmente funcional, se a partir de qualquer mundo no máximo um mundo
|
||
é acessível.
|
||
Se é o caso que de qualquer mundo exatamente um mundo é acessível, chamamo-la
|
||
funcional.
|
||
(Assim as relações funcionais são precisamente aquelas que são tanto seriais
|
||
como parcialmente funcionais).
|
||
Elas são chamadas funcionais, porque a relação de acessibilidade opera
|
||
como uma função (parcial).
|
||
Uma relação é fracamente densa se sempre que
|
||
\begin_inset Formula $Ruv$
|
||
\end_inset
|
||
|
||
, existe um
|
||
\begin_inset Formula $w$
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Quotes eld
|
||
\end_inset
|
||
|
||
entre
|
||
\begin_inset Quotes erd
|
||
\end_inset
|
||
|
||
|
||
\begin_inset Formula $u$
|
||
\end_inset
|
||
|
||
e
|
||
\begin_inset Formula $v$
|
||
\end_inset
|
||
|
||
.
|
||
\end_layout
|
||
|
||
\begin_layout Standard
|
||
\begin_inset Float table
|
||
wide false
|
||
sideways false
|
||
status open
|
||
|
||
\begin_layout Plain Layout
|
||
\align center
|
||
\begin_inset Tabular
|
||
<lyxtabular version="3" rows="6" columns="2">
|
||
<features tabularvalignment="middle">
|
||
<column alignment="left" valignment="top" width="5cm">
|
||
<column alignment="left" valignment="top">
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
|
||
\emph on
|
||
Se R é ...
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
então ...
|
||
é verdadeira em
|
||
\begin_inset Formula $\mathbf{M}$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
parcialmente funcional:
|
||
\begin_inset Formula $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow u=v)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\diamondsuit p\rightarrow\square p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
funcional:
|
||
\begin_inset Formula $\forall w\exists u\forall v(Rwu\leftrightarrow u=v)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\diamondsuit p\leftrightarrow\square p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
fracamente densa:
|
||
\begin_inset Formula $\forall u\forall v(Ruv\rightarrow\exists w(Ruw\wedge Rwv)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square\square p\rightarrow\square p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
fracamente conectada:
|
||
\begin_inset Formula $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow Ruv\vee u=v\vee Rvu)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\square((p\wedge\square p)\rightarrow q)\vee\square((q\wedge\square q)\rightarrow p)$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
<row>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
fracamente direcionada:
|
||
\begin_inset Formula $\forall w\forall u\forall v(Rwu\wedge Rwv\rightarrow\exists t(Rut\wedge Rvt))$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
<cell alignment="left" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
|
||
\begin_inset Text
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Formula $\diamondsuit\square p\rightarrow\square\diamondsuit p$
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
</cell>
|
||
</row>
|
||
</lyxtabular>
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\begin_layout Plain Layout
|
||
\begin_inset Caption Standard
|
||
|
||
\begin_layout Plain Layout
|
||
Mais cinco fatos de correspondência
|
||
\begin_inset CommandInset label
|
||
LatexCommand label
|
||
name "tabela2-2"
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_inset
|
||
|
||
|
||
\end_layout
|
||
|
||
\end_body
|
||
\end_document
|