João Marcos, Em 14 de junho de 2011 11:58, Joao Marcos <botoc...@gmail.com> escreveu:
> Talvez alguém que tenha comparecido ao WoLLIC deste ano possa nos > explicar um pouco mais sobre os tais "Univalent Foundations of > Mathematics"? > > http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/2011_WoLLIC.pdf > > Estive lá, sim. Mas não há como ser mais preciso por e-mail do que o material que ele próprio disponibiliza. Como já foi dito por Valéria, o foco não é no problema da possível (in)consistência da aritmética, mas na busca por novos fundamentos da matemática com base na teoria de tipos de Martin-Löf (alternativamente a ZFC). Como especialista em teoria da homotopia, Voevodsky está procurando encontrar paralelos entre as construções da teoria construtiva de tipos (em particular, o cálculo de construções) e os tipos de homotopia. E até mesmo implementar as construções no sistema Coq. Segundo ele mesmo diz na sua motivação, o ponto de partida foi o modelo grupóide da teoria de tipos intensional construído por Martin Hofmann e Thomas Streicher ("The Groupoid Model Refutes Uniqueness of Identity Proofs", LICS 1994). Aqui na UFPE estamos (eu e Luciana Vale, aluna do doutorado da Matemática) tentando fazer uma leitura desse modelo a partir da reformulação da interpretação funcional da igualdade proposicional que começamos a elaborar desde o 9th Amsterdam Coll (1994), e que mais recentemente foi apresentada no LSFA 2010 ("The Functional Interpretation of Direct Computations"). Propus à Matemática trazer Voevodsky para o próximo Programa de Verão. Caso se confirme, divulgo na lista. Abraço, Ruy JM > > 2011/6/6 Valeria de Paiva <valeria.depa...@gmail.com>: > > Marcelo, > > > > eu nem assisti a palestra ainda, mas todas as discusses que li, dizem que > o > > apelo 'e pra uma fundamentacao usando Martin-Loeuf's teoria de tipos. > > > > abs > > Valeria > > > > 2011/6/6 Marcelo Finger <mfin...@ime.usp.br> > >> > >> Acho que é um apelo por uma fundamentação paraconsistente. > >> > >> > >> 2011/6/6 Joao Marcos <botoc...@gmail.com> > >> > >> > "What if current foundations of mathematics are inconsistent?" > >> > - Institute for Advanced Study, Princeton > >> > http://video.ias.edu/voevodsky-80th > >> > > >> > > >> > Have fun, > >> > JM > >> > _______________________________________________ > >> > Logica-l mailing list > >> > Logica-l@dimap.ufrn.br > >> > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > >> > > >> > >> > >> > >> -- > >> Marcelo Finger > >> Departamento de Ciencia da Computacao > >> Instituto de Matematica e Estatistica > >> Universidade de Sao Paulo > >> Rua do Matao, 1010 > >> 05508-090 Sao Paulo, SP Brazil > >> Tel: +55 11 3091-9688, 3091-6135, 3091-6134 (fax) > >> http://www.ime.usp.br/~mfinger > >> _______________________________________________ > >> Logica-l mailing list > >> Logica-l@dimap.ufrn.br > >> http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > > > > > > > > -- > > Valeria de Paiva > > http://www.cs.bham.ac.uk/~vdp/ > > http://valeriadepaiva.org/www/ > > > > > > -- > http://sequiturquodlibet.googlepages.com/ > _______________________________________________ > Logica-l mailing list > Logica-l@dimap.ufrn.br > http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l > _______________________________________________ Logica-l mailing list Logica-l@dimap.ufrn.br http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
