Dúvidas de lógica para o meu eu do futuro parte 2

Atualmente estou no fim das minhas férias de janeiro. Ela durou apenas 1 mês por causa de uma greve que todas as universidades federais fizeram no ano passado.

Nesse mês em casa, eu fiz principalmente duas coisas:

joguei um jogo em que construímos um computador do zero, chamado NandGame;
li os capítulos 14 e 15 do livro de lógica do Mortari.

Considerando que eu passei as férias inteiras lendo o livro do Mortari, então faz 7 meses que eu venho lendo ele, sendo eles: 12/2023, 01/2024, 02/2024, 05/2024, 06/2024, 10/2024, 01/2025.

Logo, eu li – tentando fazer todos os exercícios – 15 capítulos do Mortari em 7 meses.

Comparando esses dados com os de outras pessoas, posso dizer que sou um aprendiz lento. Mas não tem problema!

Eu estudo porque gosto, e estudar lógica nessas férias me fez lembrar que 1 ano atrás eu queria saber o que é uma coisa se seguir da outra (e agora já tenho uma ideia!).

Dito isso, esse post é sobre as principais dúvidas que tive enquanto estudava lógica. Meu objetivo é ler essas dúvidas daqui 1 mês e meio, quando eu estiver nas minhas próximas férias.

Separei as dúvidas em duas partes: dúvidas sobre o NandGame e dúvidas sobre Lógica/Mortari.

~~desculpa pelo post de quase 2000 palavras, eu tenho muitas dúvidas :’-)~~

Lista das dúvidas:

Dúvidas sobre o NandGame

Começando com as dúvidas sobre o jogo, a primeira dúvida é:

Pra que servem os circuitos lógicos?

Pelo o que eu entendi, um computador é um gigantesco conjunto de circuitos digitais (ou circuitos lógicos). Esses circuitos são cabos onde passam energia (que eu creio ser elétrons). Cada circuito tem um ou mais inputs e somente um output. Eu não entendo nada disso, mas acho que os inputs são análogos às proposições atômicas na lógica que eu estudo.

No NandGame, as primeiras fases são para criar alguns circuitos lógicos especiais.

Isto significa que jogando o jogo eu aprendi a criar alguns circuitos lógicos interessantes. Mas… pra que servem esses circuitos?

Acho que o primeiro passo para responder essa dúvida é continuar jogando o NandGame, já que ver o resultado final deve esclarecer as coisas.

Na próxima fase do jogo eu terei que construir um somador, e isso já se parece um pouquinho mais com um computador. Mas, para essa fase eu terei que saber sobre números binários, assunto que eu nunca peguei pra estudar.

Próxima dúvida:

Como criar uma proposição a partir da sua tabela verdade?

Apesar de ter pensado nisso jogando o NandGame, essa é uma dúvida de lógica também.

Os circuitos lógicos funcionam como proposições moleculares, e todas as fases do jogo são sobre criar um circuito a partir da sua tabela verdade.

Desde cedo nos estudos de lógica, aprendemos um algoritmo para criar a tabela verdade de “qualquer” proposição molecular. No entanto, o problema do jogo é o inverso desse: temos que aprender a criar uma proposição a partir da sua tabela verdade (e com um número limitado de conectivos disponíveis).

Graças ao jogo, notei que não sei nenhum algoritmo para resolver esse problema. Sempre que me deparo com ele, tenho que usar a criatividade pra resolvê-lo.

Dúvidas sobre lógica

Agora falarei das dúvidas que tive enquanto lia o Mortari.

(assim como o Mortari, chamarei a lógica de primeira ordem de CQC e a lógica proposicional de CPC)

Como evitar a circularidade entre lógica e teoria de conjuntos?

Essa é a pior dúvida de todas, por isso começarei a parte de lógica com ela.

No livro do Mortari, trabalhamos muito com o CQC, que é a lógica de primeira ordem.

Frequentemente o Mortari prova ou enuncia teoremas sobre o CQC, isto é, metateoremas do CQC.

Mas metateoremas devem pertencer a uma metateoria, certo?

Certo. E a metateoria que o Mortari usa para o CQC é a Teoria de Conjuntos.

Sim, para provar metateoremas do CQC, ele faz as mesmas provas que eu vi nos meus cursos de álgebra, ou que estão no capítulo 1 de literalmente todo livro texto de matemática.

Mas até aqui beleza. Apesar de ser algo curioso, qual o problema com a Teoria de Conjuntos ser a metateoria da Lógica?

O problema é que a base da Teoria de Conjuntos também é a Lógica (palavras do chat gpt), então isso tudo fica circular. Se eu entendi direito, a Lógica é a metateoria da Teoria de Conjuntos também.

Eu já tinha concluído uma parte dessas coisas 3 meses atrás, quando escrevi meu outro post de dúvidas de lógica. Leia qual foi minha primeira dúvida lá:

porque a semântica para uma linguagem de primeira ordem é feita utilizando-se ferramentas da teoria de conjuntos?
Tentando responder essa dúvida, eu concluí que a semântica para uma linguagem de primeira ordem deve ser uma teoria escrita em uma outra linguagem. Então talvez a teoria de conjuntos seja essa metalinguagem em que conseguimos expressar teoremas sobre os significados dos símbolos de uma linguagem de primeira ordem. […]
De qualquer forma, o parágrafo acima é muito confuso, o que só mostra que eu de fato não entendo porque semântica formal e teoria de conjuntos estão relacionados.

(esse parágrafo não está tão confuso mais!)

No entanto, eu não tinha percebido que a Lógica é a metateoria da Teoria de Conjuntos.

Pra ser justo, ainda não tenho certeza se isso é verdade. Mas tenho certeza de que a Teoria de Conjuntos é de fato a metateoria da Lógica. Então agora que aceitei isso, consigo usar a Teoria de Conjuntos como justificativa para qualquer afirmação sobre lógica! Finalmente ter lido 12 capítulos do Halmos vai servir para alguma coisa.

A linguagem do CPC está contida na linguagem do CQC?

Note que essa é uma pergunta sobre a metalógica do CQC. Por isso terei que usar Teoria de Conjuntos para estudá-la.

Creio que se a pergunta fosse sobre os alfabetos do CPC e do CQC, a resposta seria sim, pois o alfabeto da linguagem do CQC é o alfabeto da linguagem do CPC unido com um outro conjunto.

Na metateoria, o alfabeto $A_{cpc}$ do CPC é:

$A_{cpc} = \{A \, \backslash \, A \text{ é uma letra sentencial} \} \cup \{\nao, \ou, \e, \rightarrow, \leftrightarrow, (, ) \}$

E o alfabeto $A_{cqc}$ do CQC é:

$A_{cqc} = \{a \, \backslash \, a \text{ é uma constante} \} \cup \{x \, \backslash \, x \text{ é uma váriavel} \} \cup \{A \, \backslash \, A \text{ é uma letra sentencial} \} \cup \{P \, \backslash \, P \text{ é uma constante de predicado} \} \cup \{\nao, \ou, \e, \rightarrow, \leftrightarrow, (, ) \} \cup \{\exists, \forall \}$

Logo,

$A_{cqc} = A_{cpc} \cup \{a \, \backslash \, a \text{ é uma constante} \} \cup \{x \, \backslash \, x \text{ é uma váriavel} \} \cup \{P \, \backslash \, P \text{ é uma constante de predicado} \} \cup \{\exists, \forall \}$

E, portanto $A_{cpc} \subset A_{cqc}$ .

Mas não sei se essa continência continua válida para os conjuntos que são a linguagem do CPC e do CQC. Para saber isso, eu preciso primeiro aprender a construir uma linguagem a partir do seu alfabeto primeiro.

As regras de inferência primitivas são muito arbitrárias

As regras de inferência são regras que dizem como se pode pensar dentro de uma lógica.

Elas são basicamente regras do pensamento, dizendo como você pode pensar sobre aquela linguagem para deduzir consequências lógicas. E regras assim serem arbitrárias é algo que me incomoda, pois dificulta eu lembrar delas.

Acho que a metalógica justifica essa arbitrariedade, pois nela, uma regra de inferência como a Modus Ponens é uma operação da linguagem de primeira ordem.

Se denotarmos a linguagem do CPC como $L_{cpc}$ , na metateoria definimos a Modus Ponens como:

$\begin{array}{rcl} MP: & L_{cpc} \times L_{cpc} & \to \; L_{cpc} \\ & (P, P \rightarrow Q) & \mapsto \; Q \end{array}$

E eu creio ser possível provar um metateorema que diz que existem vários conjuntos completos de regras de inferência primitivas. Disto decorreria que as outras regras de inferência são apenas uma abreviação de uma dedução natural da lógica.

O problema é que, por conta disso, dependendo do que eu escolho como regras de inferência primitivas, uma regra que você achava que era primitiva vira derivada e vice versa. Isso confunde.

Além disso, a Teoria de Conjuntos também tem suas regras. Antes de fazer tudo isso precisamos mostrar que a Modus Ponens e as outras operações existem (já que operações são conjuntos), e que elas realmente se comportam como regras de inferências. Acho que isso por si só já é muito difícil.

Por que regras de inferências derivadas são metateoremas tão estranhos?

Se regras de inferências derivadas são abreviações de deduções naturais, então são metateoremas, certo?

O problema é que são metateoremas que você prova exatamente da mesma forma que prova um teorema da lógica. Acho que esses metateoremas sejam de uma classe especial, chamada de esquemas de deduções. Por isso são provados iguais deduções da lógica.

Aliás, o exercício mais difícil dessas férias foi o de provar algumas regras de inferência derivadas do CQC. Talvez seja difícil justamente por ser um metateorema. Ele é o exercício 15.7 do livro do Mortari.

O que é uma hipótese dentro de uma dedução natural?

Há algumas regras de inferência que nos permitem inferir fórmulas a partir de hipóteses. Mas o que são essas hipóteses?

Parece muito roubado poder criar hipóteses dentro de uma demonstração. E o pior é que no sistema formal do Mortari, o CQC tem regras hipotéticas como regras primitivas! Isso quer dizer que poder fazer conclusões a partir de hipóteses é algo aceito sem questionamentos.

Você pode eliminar um existe introduzindo um para todo?

Uma regra de inferência é a eliminação do existe:

A minha dúvida é se ela permite deduções assim:

Essa dedução parece definitivamente errada, mas não consigo explicar o porque.

Essa dúvida é falta de vergonha na cara pois o livro provavelmente responde ela, mas não vou poder ler agora, então deixo pro André do futuro.

Existem teoremas do CQC, teoremas sobre o CQC e teoremas de uma teoria no CQC?

Por fim, queria entender quantos significados pra palavra teorema existem ;-;

Teoremas do CQC são proposições que decorrem de um conjunto vazio de premissas. Teoremas sobre o CQC são metateoremas da Teoria de Conjuntos.

Já teoremas de uma teoria no CQC eu não sei o que direito. Provavelmente vou aprender quando ler o capítulo 17 do livro do Mortari.

Será que isso é só um caso onde usamos o mesmo significante para vários significados?

Bônus: paradoxo de Zenão formalizado

Antes de finalizar, queria deixar registrado aqui a formalização de um dos paradoxos de Zenão. Só pra guardar em algum lugar mesmo, já que isso é super legal.

Os paradoxos de zenão são argumentos para conclusões absurdas sobre o movimento.

O Mortari formalizou um deles na linguagem de primeira de ordem. Ou melhor, deixou isso como um exercício do capítulo 15, veja:

*eu enunciaria o argumento um pouco diferente, mas a formalização seria a mesma.*

A formalização do próprio Mortari, que se encontra em seu site, é:

Note que não usamos a premissa de que tudo está em movimento ou em repouso pra nada.