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 [axioma]

2 . 2 é par [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)

P, Q

P Q

Q, P

P Q

- Intro

P Q

P

P Q

Q

- Elim

P

P Q

P

Q P

- Intro

R

- Elim

P R,Q R, P Q

Regras de Inferência (Cálculo Proposicional)

P Q, Q P

P Q

- Intro

P, P Q

Q

- Elim

P Q

P Q

- Intro

P Q

P Q

P Q

Q P

- Elim

¬ - Intro

¬ P

P Q, P ¬ Q

¬ ¬ P

P

¬ - Elim

Exercício Prove o seguinte teorema:

P Q P Q

Regras de Inferência (Cálculo de Predicados)

x . P(x)

P(a)

P(a)

x . P(x)

- Elim - Intro

- Intro

x . P(x), x . P(x) Q

Q

- Elim

Para um

arbitrário

P(a)

x . P(x)

a

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} {x:IN | x é primo x<10 . x}

{0, 2, 4, ...} {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]

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}

Provando Alguns Fatos Elementares

Versões do Axioma de Pertinência

Axioma 3. x{y:S | P(y)} (xS 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) [hipótese]

2. P(a)Q(a) [-elim]

3. a {y:S | P(y)} [hipótese]

4. a S P(a) [Axima 3]

5. P(a) [-elim]

6. Q(a) [ -elim]

7. a S [-elim]

8. a S Q(a) [7,6 -intro]

9. a {y:S | Q(y)} [Axima 3]

10. a {y:S | P(y)} a {y:S | Q(y)} [ -intro]

11. x.x{y:S | P(y)}x{y:S | Q(y)}) [-intro]

12. (x.P(x)Q(x)) (x.x{y:S | P(y)}x{y:S | Q(y)}) [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