#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