Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Hermógenes, Desculpe-me. Por favor, desconsidere o inicio da minha mensagem anterior. De fato, A \cong empty é terrível. Além de ter os mesmos problemas que A ---> empty (por exemplo, ser justificado por contra-positiva, afinal esse é o único jeito de justificar uma prova de inexistência),

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Viva, Hermógenes: > Se é que eu entendi bem o "conectivo" que você apresentou, minha > hesitação inicial diz respeito exatamente ao fato dele ser apenas > *parcialmente* determinado, isto é, sua semântica (valor semântico) > estaria fixada apenas com relação a uma parte das sentenças da >

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Hermógenes > Não. A minha sugestão é diferente. \neg A deve ser definido como A > > \cong empty := \sum_{f: A --> empty} isequ (f) . Já iseq (f) é um > > pouco mais complicado de escrever via email, portanto vou pedir que > > olhe a pagina 78 do HoTT book > > Isso não faz muito sentido para

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Fernando Yamauti escreveu: > Não. A minha sugestão é diferente. \neg A deve ser definido como A > \cong empty := \sum_{f: A --> empty} isequ (f) . Já iseq (f) é um > pouco mais complicado de escrever via email, portanto vou pedir que > olhe a pagina 78 do HoTT book Isso não

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Joao Marcos escreveu: > Assim que tivermos um critério de logicidade em mãos, portanto, > poderemos discutir melhor. :-) Eu diria que o problema não é a ausência de critérios de logicidade, mas a abundância deles. > Uma maneira de resumir o meu comentário seria: antes de

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Hermógenes, > Existe uma maneira mais construtiva de se definir a negação. Basta > > tomar \neg A como 'A não é habitado', usando tipos isso seria dado por > > uma equivalência homotopica entre A e empty (não precisa de universos > > para fazer isso). > > Sim, claro. Em termos lógicos, essa

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Viva, Valeria: > gostaria de entender melhor o que JM quer dizer com: >>note com efeito que a regra de substituição uniforme não se aplica ao >> símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a >> sentenças atômicas. > > da' pra repetir a ideia aqui? Vou tentar. A

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

ok mais 2 centavos daqui de longe: gostaria de entender melhor o que JM quer dizer com: >note com efeito que a regra de substituição uniforme não se aplica ao símbolo de absurdo, como um *conectivo* nulário, tal como se aplica a sentenças atômicas. da' pra repetir a ideia aqui? como eu passei

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi JM e Hermógenes, Um breve comentário sobre o top. Em uma mensagem anterior, JM escreveu: Hummm... Dualmente, qual seria a regra de eliminação do top? A regra > de que "sob nenhuma circunstância podemos eliminar o top"? Parece-me > um simples forçação de barra. Podemos eliminá-lo sim e

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Salve, Hermógenes: Obrigado pela resposta. >>> Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, >>> (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no >>> caso da negação definida pelo absurdo), e (2) seja construtivamente >>> justificável. >>> >>> Se

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Joao Marcos escreveu: >> Bem, o problema é o que colocar no lugar de ECQ que, ao mesmo tempo, >> (1) seja razoável se chamar de "negação" (ou, melhor, "absurdo", no >> caso da negação definida pelo absurdo), e (2) seja construtivamente >> justificável. >> >> Se permanecemos

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Bruno Bentzen escreveu: > Oi Hermógenes, Olá, Bruno. > [...] > > PS: Posso estar enganado, mas acho um pouco equivocado e confuso usar > a palavra “completude” (um termo de cunho técnico ou meta-matemático) > neste caso quando estamos nos tratando de uma semântica

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Viva, Hermógenes: Obrigado pela resposta. >>> Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O >>> difícil é que, sem ECQ, um construtivista ficaria basicamente sem >>> negação (ao estilo do cálculo mínimo de Johansson), ou a negação >>> cessaria de ser um operador *lógico*. >> >>

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Fernando Yamauti escreveu: > Oi Hermógenes, Olá, Fernando. > Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O difícil é > que, sem ECQ, um construtivista ficaria basicamente sem negação (ao > estilo do cálculo mínimo de Johansson), ou a negação cessaria de

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Joao Marcos escreveu: >> Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O >> difícil é que, sem ECQ, um construtivista ficaria basicamente sem >> negação (ao estilo do cálculo mínimo de Johansson), ou a negação >> cessaria de ser um operador *lógico*. > > Por quê,

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Hermógenes, [...] Neste ponto, a única vantagem de TIT em comparação à ZF (sua > concorrente igualmente ad hoc), principalmente se você é um computeiro > ou matemático preocupado com computabilidade, é o fato de TIT ser > construtiva. Retomando um pouco o ponto da Valéria sobre a

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Hermógenes, Obrigado pelas referências. Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O difícil é > que, sem ECQ, um construtivista ficaria basicamente sem negação (ao > estilo do cálculo mínimo de Johansson), ou a negação cessaria de ser um > operador *lógico*. Uma

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

> Eu, pessoalmente, acho ECQ um princípio *muito* suspeito. O difícil é > que, sem ECQ, um construtivista ficaria basicamente sem negação (ao > estilo do cálculo mínimo de Johansson), ou a negação cessaria de ser um > operador *lógico*. Por quê, Hermógenes? > Martin-Löf, no artigo de

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

meus dois centavos nessa discussao (so' pra voces nao ficarem com a impressao de que ninguem le...): 1.>Muitos, porém, acham o preço a se pagar muito salgado: falha da transitividade (monotonicidade, regra de corte). eu acho um preco absurdo. pior do que se tem que pagar por chifre de unicornio!

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

1. Eu trabalhei com pragmática do ponto de vista da lógica. A questão extrapola os limites da linguagem ao invés de encontrar soluções nela. Até porque a análise pragmática de fenômenos linguísticos remete a um nível de abstração ainda mais alto, onde a distinção entre linguagem e pensamento

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Eu escrevi: > [...] > > Uma exceção interessante é o caso da "Core Logic" de Tennant, onde a > negação é dada um caráter lógico, mesmo sem ECQ, pela admissão de > modus tollendo ponens (ou silogismo disjuntivo) e uma regra especial > para a implicação que permite obter ¬A,A⊢B. [...] Ops.

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Fernando Yamauti escreveu: > [...] > > Um outro caso que me incomoda muito e o Martin-Löf sempre joga em > baixo do tapete: o porquê de " 'A true' infere 'B true' " ser > correto, onde A é falso (onde o "falso" é clássico, ou seja, existe > uma prova de \neg A) , para um

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Fernando, Também há outra razão para achar as justificativas acima mencionadas insuficientes. Uma vez que o caráter computacional da HoTT (na sua caracterização padrão descrita no livro) é desconhecido, a teoria como um todo seria destituida de qualquer significado ou base filosófica -

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Bruno, Obrigado pelas referencias. Eu já conhecia todas elas menos a do Walsh (que vou ler depois com mais calma, mas aparentemente o que ele faz é pegar a imagem da diagonal pelo elemento final da fibra em A, mas isso leva a um problema semelhante ao do artigo do Ladyman e Presnell, já

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Melhor considerar exemplos específicos. Sent from my iPhone > On 4 Apr 2017, at 10:10, Bruno Bentzen wrote: > > Oi Fernando, > > Talvez você possa se interessar também por esta animada discussão na FOM > > https://www.cs.nyu.edu/pipermail/fom/2016-March/019575.html >

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi Fernando, Talvez você possa se interessar também por esta animada discussão na FOM https://www.cs.nyu.edu/pipermail/fom/2016-March/019575.html que chegou a ser uma thread bem animada no mês de março do ano passado (inclusive este paper é mencionado). O Ladyman e o Presnell parecem ter

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Muito obrigado! Em 3 de abril de 2017 13:28, Hermógenes Oliveira < hermogenes.olive...@student.uni-tuebingen.de> escreveu: > Fernando Yamauti escreveu: > > > Oi, > > > > Será que alguém teria acesso ao paper > > > > 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type

Re: [Logica-l] Philosophia Mathematica Vol 23 Issue 3

Fernando Yamauti escreveu: > Oi, > > Será que alguém teria acesso ao paper > > 1 Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I: > The Justification of Path Induction. Philosophia Mathematica (2015) ? Coincidência. Eu li esse artigo recentemente. A

[Logica-l] Philosophia Mathematica Vol 23 Issue 3

Oi, Será que alguém teria acesso ao paper 1. Ladyman, J., Presnell, S.: Identity in Homotopy Type Theory, Part I: TheJustification of Path Induction. Philosophia Mathematica (2015)