Grupo de Lógica - dia 30/09

Olá para todos.

No próximo encontro do grupo de lógica, que terá início às 17h no local de sempre, veremos os seguintes tópicos do livro da Negri:

Teorema 2.5.6 - sequentes não-demonstráveis na lógica intuicionista (em G3ip) - p.43

Independência dos conectivos na lógica intuicionista - p. 45

A definição de trace formula - p. 51

Teorema 3.1.4 - equivalência entre C e a conjunção das trace formulas de C - p. 51

Os capítulos correspondentes já foram disponibilizados.

Abraços

Regras inversíveis - G3ip

Abaixo, apostilas sobre equivalência entre G1ip e G3ip
http://dl.dropbox.com/u/5959592/eqvl_g1ip_g3ip.pdf
e sobre regras inversíveis em G3ip
http://dl.dropbox.com/u/5959592/regras_inver_G3ip.pdf
abraços

Algumas provas em G1

Olá para todos.
Abaixo, uma apostila com algumas provas em G1 (mais precisamente, G1ip, i.e. G1 para lógica proposicional intuicionista, que vimos no último encontro).
http://dl.dropbox.com/u/5959592/G1.pdf
Minha sugestão é que vocês peguem alguma lista de tautologias - do
Mortari por exemplo - e verifiquem com G1ip todas que valem
intuicionisticamente.
Abraços

Texto Kolmogorov e encontro da próxima quinta

Olá para todos.

Para quem estiver interessado, na próxima quinta-feira às 17h faremos um revisão do que já foi visto em sistemas axiomáticos e dedução natural. 

O horário das 18h fica mantido

Abaixo, um pdf do texto do Kolmogorov sobre o terceiro excluído.
http://dl.dropbox.com/u/5959592/kolmogorov_excluded_middle_heijnoort.pdf

Abraços

Material disponível e outros assuntos

Olá para todos.

No último encontro do grupo de lógica vimos como transformar provas em
dedução natural em provas em sistemas de Hilbert e vice-versa. Usamos
as apostilas abaixo
http://dl.dropbox.com/u/5959592/hilbert_prop.pdf
http://dl.dropbox.com/u/5959592/Hilbert_DN.pdf

Há também uma lista de exercícios no link
http://dl.dropbox.com/u/5959592/exercicios_H_DN.pdf

E no link
http://dl.dropbox.com/u/5959592/books/NEGRI_intro_1.pdf
está a introdução e o capítulo 1 da Negri e von Plato, From natural

deduction to sequent calculus.

Quem estiver com dúvidas e quiser fazer uma revisão sobre dedução
natural e sistemas axiomáticos podemos marcar um horário às 17h, antes
do grupo. Envie email para abilio.arf@gmail.com.
Mas o horário do grupo continua sendo 18h.

Abaixo, algumas leituras recomendadas para quem estiver interessado
nas motivações filosóficas e aspectos históricos das lógicas
intuicionista e minimal.

Um capítulo do livro da Maria da Paz, Traduções via teoria da Prova:
aplicações à lógica linear, 2002, EDUFRN
http://dl.dropbox.com/u/5959592/books/dapaz.pdf

Verbetes da Stanford sobre intuicionismo,
http://plato.stanford.edu/entries/logic-intuitionistic/
http://plato.stanford.edu/entries/intuitionistic-logic-development/
e teoria da prova
http://plato.stanford.edu/entries/proof-theory-development/

Vale a pena também ler o texto do Kolmogorov, On the principle of
excluded middle.  Está na coletânea do van Heijenoort, From Frege to
Gödel.

E abaixo
http://dl.dropbox.com/u/5959592/books/gentzen_logical_deduction.pdf
o texto do Gentzen, Investigations into logical deduction.

Abraços