| 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.: aprender ≠ passar.)
Além disso, é necessário que tu tens tempo e vontade para estudar, fazer os trabalhos atribuídos, etc.
(Obs.: estudar ≠ ler.)
Antes de começar é bom dar uma lida nos:
- Comments on style de Munkres.
- 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
- Eu: Matemática fundacional para computação [fmcbook] (Capítulos 1–2)
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
- James Munkres: Comments on style
- Jean-Pierre Serre: How to write mathematics badly
- Don Knuth: Mathematical writing
- Paul Halmos: How to write mathematics
- Por que tantos livros? Qual é o melhor? Vale a pena ler esse excerto do livro Linear Algebra de Jänich.
Links
- NNG (Offline? Tente esse mirror também.)
- Lean & Lean web editor
- Haskell
- Minicurso TeX 2018.2
- Detexify
- Minicurso Unix 2019.2
- The Missing Semester of your CS Education
- Overleaf online (La)TeX editor/compilador
Tecnologias & ferramentas
(Instalem e/ou criem uma conta para usar onde necessário.)
- PAPEL (um caderno para dedicar à disciplina) e LAPIS/CANETA.
- O proof assistant Lean para algumas atividades (leia o FAQ).
- Git (leia o FAQ).
- Muito recomendado mas não necessário: um sistema Unix (veja o minicurso Unix 2019.2).
- Muito recomendado mas não necessário: (neo)vim e Emacs.
- Pouco de (La)TeX (veja o minicurso TeX 2018.2). Online editor/compilador: Overleaf.
FAQs
Dynamic content
Provas
- Prova 1.0 de FMC1 de 2022.2: Tutorial World (NNG)
- Prova 1.1 de FMC1 de 2022.2 { censored , uncensored , answers , correções }
- Prova 1.2 de FMC1 de 2022.2: logic.lean
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
- 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
- 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
- Demonstre os teoremas seguintes escrevendo demonstrações “low-level”, mantendo também os DADOS/ALVO atualizados com cada linha da sua demonstração:
- Θ. Todo inteiro divide ele mesmo.
- Θ. Para quaisquer inteiros a,b, se a divide b e b divide 0, então a divide 0 ou 1 divide b.
- Θ. Seja a inteiro. Para quaisquer inteiros x,y, se a | x e a | y, então a | x + y.
- Θ. Seja a inteiro. Para todo inteiro x, se a | x, então para todo inteiro u, a | ux.
- Θ. Para quaisquer inteiros a,x,y,r,s, se a | x e a | y, então a | rx + ys.
- 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
- 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!
- Proposições de dupla negaço:
- P ⇒ ¬¬P
- ¬¬P ⇒ P
- Comutatividade dos ∨,∧:
- (P ∨ Q) ⇒ (Q ∨ P)
- (P ∧ Q) ⇒ (Q ∧ P)
- Proposições de interdefinabilidade dos ⇒,∨:
- (P ⇒ Q) ⇒ (¬P ∨ Q)
- (P ⇒ Q) ⇐ (¬P ∨ Q)
- (P ∨ Q) ⇒ (¬P ⇒ Q)
- (P ∨ Q) ⇐ (¬P ⇒ Q)
- Proposições de contraposição:
- (P ⇒ Q) ⇒ (¬Q ⇒ ¬P)
- (¬Q ⇒ ¬P) ⇒ (P ⇒ Q)
- A irrefutabilidade do LEM:
- ¬¬(P∨¬P)
- A lei de Peirce e sua versão “fraca”:
- ((P ⇒ Q) ⇒ P) ⇒ P
- ((P ⇒ Q) ⇒ P) ⇒ ¬¬P
- Proposições de interdefinabilidade dos ∨,∧:
- P∨Q ⇒ ¬(¬P∧¬Q)
- P∨Q ⇐ ¬(¬P∧¬Q)
- P∧Q ⇒ ¬(¬P∨¬Q)
- P∧Q ⇐ ¬(¬P∨¬Q)
- As leis de De Morgan para ∨,∧:
- ¬(P∨Q) ⇒ (¬P ∧ ¬Q)
- ¬(P∨Q) ⇐ (¬P ∧ ¬Q)
- ¬(P∧Q) ⇒ (¬Q ∨ ¬P)
- ¬(P∧Q) ⇐ (¬Q ∨ ¬P)
- Proposições de distributividade dos ∨,∧:
- P∧(Q∨R) ⇒ (P∧Q)∨(P∧R)
- P∧(Q∨R) ⇐ (P∧Q)∨(P∧R)
- P∨(Q∧R) ⇒ (P∨Q)∧(P∨R)
- P∨(Q∧R) ⇐ (P∨Q)∧(P∨R)
- Currificação
- ((P∧Q)⇒R) ⇒ (P⇒(Q⇒R))
- ((P∧Q)⇒R) ⇐ (P⇒(Q⇒R))
- Reflexividade da ⇒:
- P ⇒ P
- Weakening and contraction:
- P ⇒ (P∨Q)
- Q ⇒ (P∨Q)
- (P∧Q) ⇒ P
- (P∧Q) ⇒ Q
- P ⇒ (P∧P)
- (P∨P) ⇒ P
- As leis de De Morgan para ∃,∀:
- ¬(∀x)[φ(x)] ⇒ (∃x)[¬φ(x)]
- ¬(∀x)[φ(x)] ⇐ (∃x)[¬φ(x)]
- ¬(∃x)[φ(x)] ⇒ (∀x)[¬φ(x)]
- ¬(∃x)[φ(x)] ⇐ (∀x)[¬φ(x)]
- Proposições de interdefinabilidade dos ∃,∀:
- (∃x)[φ(x)] ⇒ ¬(∀x)[¬φ(x)]
- (∃x)[φ(x)] ⇐ ¬(∀x)[¬φ(x)]
- (∀x)[φ(x)] ⇒ ¬(∃x)[¬φ(x)]
- (∀x)[φ(x)] ⇐ ¬(∃x)[¬φ(x)]
- Proposições de distributividade de quantificadores:
- (∃x)[φ(x) ∧ ψ(x)] ⇒ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
- (∃x)[φ(x) ∧ ψ(x)] ⇐ (∃x)[φ(x)] ∧ (∃x)[ψ(x)]
- (∃x)[φ(x) ∨ ψ(x)] ⇒ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
- (∃x)[φ(x) ∨ ψ(x)] ⇐ (∃x)[φ(x)] ∨ (∃x)[ψ(x)]
- (∀x)[φ(x) ∧ ψ(x)] ⇒ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
- (∀x)[φ(x) ∧ ψ(x)] ⇐ (∀x)[φ(x)] ∧ (∀x)[ψ(x)]
- (∀x)[φ(x) ∨ ψ(x)] ⇒ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
- (∀x)[φ(x) ∨ ψ(x)] ⇐ (∀x)[φ(x)] ∨ (∀x)[ψ(x)]
- Proposições de dupla negaço:
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!