self study IntroProof

Contato:thanos@imd.ufrn.br
Playlist: IntroProof
Monitoria/TA: fmc.imd.ufrn.br
Turmas self: ../
Turmas FMC1: /teaching/fmc1

Info

Pré-requisitos

Quase nada. Apenas o conteúdo de matemática do ensino médio. Umas referências para esses conteúdos são as seguintes:

  • Lang: Basic Mathematics (de uma olhada nesta playlist no YouTube que tem um curto videozinho para cada secção deste livro)
  • Lima et al: A Matemática do Ensino Médio, vol I (para esta disciplina os mais relevantes pré-requisitos são os Cap. 1–4)

Realidade. Depois de perceber que, sistematicamente, praticamente todos os alunos que foram aprovados na disciplina de Geometria Euclideana sequer escreveram nem uma linha de demonstração matemática, eu não tenho como considerar que os alunos da turma cumprem mesmo essa parte essencial¹ de pré-requisito “oficial”.

¹ Imagine chegar em Polo Aquático I, sem ter aprendido mesmo as Natação I e II primeiro; ainda mais sem sequer ter entrado na agua na sua vida inteira!

(Obs.: aprenderpassar.)

Além disso, é necessário que tu tens tempo e vontade para estudar, fazer os trabalhos atribuídos, etc.

(Obs.: estudarler.)

Antes de começar é bom dar uma lida nos:

  1. Comments on style de Munkres.
  2. A parte “Writing mathematics” do livro The tools of mathematical reasoning, de Lakins.

Conteúdo

Introdução comum para as: IDMa, IRI, IDMb.

Bibliografia e referências

Conhece o libgen?

Principal

Auxiliar

  • Avigad, Lewis, van Doorn (2017): Logic and Proof (Cap. 17)
  • Avigad, Leonardo de Moura, and Soonho Kong (2017): Theorem proving in Lean (Cap: 7,8)
  • Daepp, Gorkin (2011): Reading, Writing, and Proving, 2nd ed.

Para cada um dos assuntos que tratamos, procure também a secção «Leitura complementar» no capítulo correspondente do fmcbook para mais referências.

Dicas

Links

Tecnologias & ferramentas

(Instalem e/ou criem uma conta para usar onde necessário.)

  1. PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA.
  2. O proof assistant Lean para algumas atividades (leia o FAQ).
  3. Git (leia o FAQ).
  4. Muito recomendado mas não necessário: um sistema Unix (veja o minicurso Unix 2019.2).
  5. Muito recomendado mas não necessário: (neo)vim e Emacs.
  6. Pouco de (La)TeX (veja o minicurso TeX 2018.2). Online editor/compilador: Overleaf.

FAQs

Dynamic content

Provas

Sessões

Leia bem o FAQ sobre hw. Note também que:

  • Homeworks são atribuidos também durante as aulas e no Zulip.
  • Homeworks marcados assim são auxiliares; tente apenas se tu tem resolvido uma parte satisfatória dos outros.

IntroProof (1): Overview; tipos [video]

  • Overview
  • tipos e type errors
  • proposiões vs objetos
  • Prop vs Bool

hw

  1. Capítulo 1.

IntroProof (2): Definições [video]

  • intensão vs extensão
  • = vs ⇔
  • «def»
  • comandos vs proposições
  • REPL
  • Exemplos de teoremas e seus tabuleiros (estados) iniciais
  • Dados e Alvo
  • açúcar sintáctico
  • sintaxe vs semântica
  • variáveis ligadas vs livres
  • escopos de variáveis
  • capturamento de variável
  • definição e seu contexto
  • escolha boa de variável, variável fresca
  • bairros de variáveis
  • os ¬,⇒,⇔,&,ou,∀,∃,=

hw

  1. Capítulo 2.

Prova 1.0

Complete o «Tutorial World» do Natural Number Game. Veja o FAQ relevante também.

IntroProof (3): Demonstrações [video]

  • ocorrências ligadas vs livres de variáveis e ligadores
  • sombreamento (shadowing) de variáveis
  • Propriedades da igualdade: refl, sym, trans, e substituição
  • «Calculamos»: seu uso, sua escrita, e seus efeitos
  • definições como abreviações

hw

  1. Demonstre os teoremas seguintes escrevendo demonstrações “low-level”, mantendo também os DADOS/ALVO atualizados com cada linha da sua demonstração:
    1. Θ. Todo inteiro divide ele mesmo.
    2. Θ. Para quaisquer inteiros a,b, se a divide b e b divide 0, então a divide 0 ou 1 divide b.
    3. Θ. Seja a inteiro. Para quaisquer inteiros x,y, se a | x e a | y, então a | x + y.
    4. Θ. Seja a inteiro. Para todo inteiro x, se a | x, então para todo inteiro u, a | ux.
    5. Θ. Para quaisquer inteiros a,x,y,r,s, se a | x e a | y, então a | rx + ys.
  2. Para cada um dos ¬,⇒,&,ou,⇔,∀,∃,= pense como que pode ser usado (sendo nos DADOS) ou atacado (sendo no ALVO). Escreva os comandos correspondentes e para cada um deles, esclareça: qual é o efeito no tabuleiro da demonstração (tanto na parte dos DADOS quanto no ALVO), como e quando é que tal comando pode ser executado.

IntroProof (4): Demonstrações [video]

  • o resto dos conectivos para nossa linguagem de demonstrações
  • os ⇔, ¬, ⇐, como açúcar sintáctico
  • o ⊥ como conectivo primitivo
  • umas “leis de lógica” e como demonstrá-las

hw

  1. Para cada uma das proposições seguintes tente demonstrar escrevendo na linguagem de demonstrações que elaboramos nas aulas até agora. Se colar em algum sem conseguir fechar, mostre teu progresso no zulip e peça ajuda; enquanto isso, continua para a próxima!
    1. Proposições de dupla negaço:
      1. P ⇒ ¬¬P
      2. ¬¬P ⇒ P
    2. Comutatividade dos ∨,∧:
      1. (P ∨ Q) ⇒ (Q ∨ P)
      2. (P ∧ Q) ⇒ (Q ∧ P)
    3. Proposições de interdefinabilidade dos ⇒,∨:
      1. (P ⇒ Q) ⇒ (¬P ∨ Q)
      2. (P ⇒ Q) ⇐ (¬P ∨ Q)
      3. (P ∨ Q) ⇒ (¬P ⇒ Q)
      4. (P ∨ Q) ⇐ (¬P ⇒ Q)
    4. Proposições de contraposição:
      1. (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
      2. (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
    5. A irrefutabilidade do LEM:
      1. ¬¬(P∨¬P)
    6. A lei de Peirce e sua versão “fraca”:
      1. ((P ⇒ Q) ⇒ P) ⇒ P
      2. ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
    7. Proposições de interdefinabilidade dos ∨,∧:
      1. P∨Q ⇒ ¬(¬P∧¬Q)
      2. P∨Q ⇐ ¬(¬P∧¬Q)
      3. P∧Q ⇒ ¬(¬P∨¬Q)
      4. P∧Q ⇐ ¬(¬P∨¬Q)
    8. As leis de De Morgan para ∨,∧:
      1. ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
      2. ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
      3. ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
      4. ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
    9. Proposições de distributividade dos ∨,∧:
      1. P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
      2. P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
      3. P∨(Q∧R) ⇒ (P∨Q)∧(P∨R)
      4. P∨(Q∧R) ⇐ (P∨Q)∧(P∨R)
    10. Currificação
      1. ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
      2. ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
    11. Reflexividade da ⇒:
      1. P ⇒ P
    12. Weakening and contraction:
      1. P ⇒ (P∨Q)
      2. Q ⇒ (P∨Q)
      3. (P∧Q) ⇒ P
      4. (P∧Q) ⇒ Q
      5. P ⇒ (P∧P)
      6. (P∨P) ⇒ P
    13. As leis de De Morgan para ∃,∀:
      1. ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
      2. ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
      3. ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
      4. ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
    14. Proposições de interdefinabilidade dos ∃,∀:
      1. (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
      2. (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
      3. (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
      4. (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
    15. Proposições de distributividade de quantificadores:
      1. (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
      2. (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
      3. (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
      4. (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
      5. (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
      6. (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
      7. (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
      8. (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]

Prova 1.1

IntroProof (5): Demonstrações [video]

  • Proposição mais forte vs mais fraca que outra
  • P ⇒ ¬¬P
  • ¬¬(P ∨ ¬P)
  • ¬¬P ⇒ P
  • RAA (Reductio ad Absurdum)
  • LEM (Law of Excluded Middle)
  • Matemática não-construtiva

Prova 1.2

Demonstre os teoremas do hw anterior no Lean (veja o FAQ!): baixe o arquivo logic.lean que tem os enunciados prontos, e o coloca na pasta fmclean/src; substitua todos os sorry, do arquivo com código que compila para demonstrar tudo. Dúvidas nos #proofassistants e #tech, obviamente!

Last update: Tue Dec 19 18:47:41 -03 2023