Modelos Matemáticos



Usados como tipos em especificações
baseadas em modelos
Apresentados como teorias ou sistemas
formais
Uma teoria é definida em termos de:
– Linguagem formal
– Axiomas
– Regras de Inferência
Teorias: conceitos adicionais


Teoremas são fórmulas derivadas dos
axiomas usando-se regras de inferência
A derivação ou prova de uma fórmula
A a partir de um conjunto P de fórmulas
é uma seqüência cuja última fórmula é
A e cada fórmula na seqüência é:
– um axioma
– uma premissa (hipótese) - elemento de P
– conseqüência de uma fórmula anterior
produzida por uma regra de inferência
Exemplo

Linguagem:
sentença :: nat é par
nat :: 0 | 1 | 2 | ...


Axioma: 0 é par
Regra de Inferência: se n é par então n + 2
é par


Teorema: 2 é par
Derivação (prova)
1 . 0 é par
2 . 2 é par
[axioma]
[1, regra de inferência]
Exemplo: Cálculo Proposicional

Linguagem:
sentença :: P | Q | R | ...
|  sentença
| sentença  sentença
| sentença  sentença
| sentença  sentença
| sentença  sentença

Axioma: ---
Regras de Inferência
(Cálculo Proposicional)
 - Intro
 - Elim
P, Q
Q, P
PQ
PQ
 - Intro
PQ
PQ
P
Q
 - Elim
P
P
PQ
QP
P R, Q
R, P  Q
R
Regras de Inferência
 - Intro
P
Q
PQ
 - Intro
P  Q, Q  P
PQ
(Cálculo Proposicional)
 - Elim
¬ - Intro
P, P  Q
P
Q, P
¬Q
¬P
Q
 - Elim
¬ - Elim
PQ
P Q
¬¬P
PQ
QP
P
Exercício

Prove o seguinte teorema:
PQ
PQ
Regras de Inferência
(Cálculo de Predicados)
 - Elim
 - Intro
x . P(x)
P(a)
P(a)
x . P(x)
 - Intro
Para um a
arbitrário
 - Elim
P(a)
x . P(x), x . P(x)  Q
x . P(x)
Q
Exercício

Prove o seguinte teorema:
P(m), x . (P(x)  Q(x))
Q(m)
Teoria de Conjuntos



Conjuntos são coleções de elementos
onde a ordem e a repetição de
elementos são irrelevantes
Existem dois tipos de representação:
Por extenso Compreensão
{e1, ..., en}
{x:S | P(x) . t(x)}
Exemplos
{2, 3, 5, 7}
{0, 2, 4, ...}
{x:IN | x é primo  x<10 . x}
{x:IN | true . 2 * x}
{0, 2, 4, 6}
{x:IN | x<4 . 2 * x}
Teoria de Conjuntos


Abreviações
{x:S . t(x)} = {x:S | true . t(x)}
{x:S | P(x)} = {x:S | P(x) . x}
Portanto,
{x:IN . 2 * x} = {x:IN | true . 2 * x}
{x:IN | x é primo  x<10} =
{x:IN | x é primo  x<10. x}
Uma Operação Básica:
Pertinência



xS
x  S = (x  S)
{x:S | P(x) . T(x)} = {x | x  S  P(x) . T(x)}
Axiomas Fundamentais


Axioma 1. Uma expressão pertence a
um conjunto se e somente se tal
expressão é igual a um dos elementos
deste conjunto:
x  {e1, ..., en}  (x=e1  ...  x=en)
Axioma 2. Extensionalidade
(S=T)  (x . x  S  x  T)
 (x . x  S  x  T) 
(x . x  T  x  S)
Provando Alguns Fatos
Elementares

Lema 1. Cada elemento do conjunto {1, 2}
é também um elemento do conjunto {2, 1}
x . x  {1, 2}  x {2,1}
Prova:
1. x  {1, 2}
[Hipótese]
2. x=1  x=2
[Axioma 1]
3. x=2  x=1
[Comut. de ]
4. x  {2, 1}
[Axioma 1]
5. x{1, 2}x{2, 1}
[ - Intro]
6. x.x{1, 2}x{2, 1} [ - Intro]
Provando Alguns Fatos
Elementares

Lema 2. Cada elemento do conjunto
{2,1} é também um elemento do
conjunto {1,2}
x . x  {2, 1}  x {1, 2}
Prova. Simétrica a do Lema 1.
Provando Alguns Fatos
Elementares

Teorema {1, 2}={2, 1}
Prova.
1. x.x{1,2}x{2,1} [Lema 1]
2. x.x{2,1}x{1,2} [Lema 2]
3. x.x{1,2}x{2,1}  [ -Intro]
x.x{2,1}x{1,2}
4. {1,2} = {2,1}
[Axioma 2]

Exercício: Prove que {2,2}={2}
Versões do Axioma de
Pertinência



Axioma 3. x{y:S | P(y)}  (xS  P(x))
Axioma 4. x{y:S . t(y)}  (y:S . x=t(y))
Axioma 5. x{y:S | P(y) . t(y)} 
(y:S | P(y) . x=t(y))
Exercício
Prove o seguinte teorema
 Teorema. A substituição de um predicado
(numa representação de conjuntos por
compreesão) por um predicado mais fraco
pode resultar num conjunto maior.
(x.P(x)Q(x))
(x.x{y:S | P(y)}x{y:S | Q(y)})
Resolução
Teorema: (x.P(x)Q(x)) (x.x{y:S | P(y)}x{y:S | Q(y)})
1.  x. P(x)Q(x)
2. P(a)Q(a)
3. a  {y:S | P(y)}
4. a S  P(a)
5. P(a)
6. Q(a)
7. a  S
8. a  S  Q(a)
9. a  {y:S | Q(y)}
10. a  {y:S | P(y)}  a  {y:S | Q(y)}
11. x.x{y:S | P(y)}x{y:S | Q(y)})
12. (x.P(x)Q(x))
(x.x{y:S | P(y)}x{y:S | Q(y)})
[hipótese]
[-elim]
[hipótese]
[Axima 3]
[-elim]
[ -elim]
[-elim]
[7,6 -intro]
[Axima 3]
[ -intro]
[-intro]
[1-11  -intro]
Conjunto Vazio: {}
Axioma 6.
 x . x  {}
ou equivalentemente:
x . ( x  {})
ou ainda:
x . ( x  {})

Subconjuntos: 
Definição. (S  T)  (x . x  S  x  T)
Teoremas:
(S = T)  (S  T  T  S)
(S  T)  (S  T  (S = T))
(S  T)  (S  T)
S . {}  S
S . S  S
Conjunto das Partes: |P
Definição. (T  |P S)  (T  S)
Teoremas:
S . {}  |P S
S . S  |P S
Produto Cartesiano: 
Definição.
p  (S  T)   y, z . p = (y, z)  y  S  z  T
Usando a notação de compreensão, temos:
(S  T) = {y : S; z : T . (y, z)}
Alguns operadores auxiliares
Funções de projeção sobre pares:
first (y, z) = y
second (y, z) = z
Cardinalidade de conjuntos finitos:
#S
Referências


Seção 4.1 do livro The Z Notation
Capítulo 5 do livro Using Z