Este documento faz parte da [Proposta 2022 de Thanos][main].

[main]: /HTv-fjHGRseioBgvKYqf0w
[CDI]: /Rsz0UzVkT8SAb5doFQA11Q

--------

[TOC]

--------

# IDM: Introdução à Demonstração Matemática (30h+30h)

## Resumo

Usamos elementos da teoria dos números inteiros e da teoria axiomática dos números reais para introduzir o aluno ao **pensamento matemático** e o processo de definir conceitos, enunciar e demonstrar teoremas.

Aproveitamos o desenvolvimento do conteúdo concreto para chegar até os seguintes conceitos fundamentais:

* congruência e aritmética modular (IDMa)
* ínfimo, supremo, sequência, limite (IDMb)

Sobre a **separação em módulos de 30h** veja a observação relevante no [documento principal da proposta][main], copiada aqui:

> A separação em módulos de 30h (que podem ser lecionados em metade de semestre cada, tendo aulas 4h/semana) *permite aos alunos que foram aprovados em apenas um dos dois não precisar repetir ambos*.
>
> Além disso as dependências das disciplinas dos semestres seguintes são especificadas para *permitir ao aluno que reprovou em um dos dois módulos conseguir cursar disciplinas dos próximos semestres sem ficar preso até aprovar no outro módulo também*.

**Recomendado:** ambas as IDMa e IDMb podem ser auxiliadas usando um *proof assistant* (e.g. Lean, Agda, Coq, ...)

## Ementas detalhadas

> [color=magenta]
>
> Θ = Teorema.

### IDMa: Elementos da teoria dos números inteiros

1. Axiomas sobre os inteiros (domínio de integridade bem ordenado).
2. Demonstrações dos primeiros teoremas pelos axiomas, sobre as operações e as relações de ordem nos inteiros.
* unicidade da $(+)$-identidade ($0$)
* unicidade da $(·)$-identidade ($1$)
* leis de $(+)$-cancelamento
* unicidade dos $(+)$-inversos (opostos)
* $0$ é um $(\cdot)$-anulador: $0\cdot x = 0 = x\cdot 0$
* $-(-x) = x$
* $(-1)x = -x$
* $(-x)y = -(xy) = x(-y)$
* $(-x)(-y) = xy$
* leis de $(\cdot)$-cancelamento
* as relações de ordem $(<,\leq,>,\geq)$ e o módulo $|-|$: definições e propriedades
* $x\neq 0 \implies x^2 > 0$
* não existe inteiro entre $0$ e $1$
1. A relação de divisibilidade e a verificação de suas principais propriedades.
* $|$ é uma preordem
* qualquer inteiro divide o $0$
* os $1,-1$ dividem qualquer inteiro
* $d \mid a\ \&\ d \mid b \implies d \mid ax + by$
* $a \mid b\ \&\ b \mid a \implies |a| = |b|$
1. Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva.
1. Lema de divisão de Euclides.
https://en.wikipedia.org/wiki/Euclidean_division
1. Números, numerais, dígitos: demonstração que qualquer inteiro b > 1, serve como base para um sistema posicional de numerais para inteiros.
1. Lema de Euclides e sua generalização.
https://en.wikipedia.org/wiki/Euclid%27s_lemma
1. Teorema Fundamental da Aritmética.
https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic
1. mdc e mmc e demonstrações das suas propriedades
* unicidade dos mdc e mmc e dualidade
* $(a,b) = (a,-b) = (-a,b) = (-a,-b)$
* $(a,a) = a$
* $(a,0) = a$
* $(a,1) = 1$
* $a \mid b \implies (a,b) = a$
* $(a,b) = (a-b,b)$
* $(a,b) = (a, na + b)$
* comutatividade: $(a,b) = (b,a)$
* associatividade: $(a,(b,c)) = ((a,b),c)$
1. Conjunto fechado sob operações
* Θ: se $C$ é fechado sobre subtração então existe $a∈C$ tal que $C = \{ a i \mid i \in ℤ \}$
* Corolário: existência de mdc e os coeficientes Bézout
1. Algoritmo de Euclides: corretude e terminação
1. Algoritmo estendido de Euclides
1. Demonstração do teorema Fundamental de Aritmética
1. Congruência módulo um inteiro e demonstrações das suas propriedades
1. Aritmética modular e propriedades do $ℤ/mℤ$.
* clásses de congruência
* invertibilidade módulo $m$
* unicidade de inverso módulo $m$
1. Algumas conjecturas da teoria dos números:
Collatz; Goldbach; Primos gêmeos; Fermat (teorema Wiles)
https://en.wikipedia.org/wiki/Collatz_conjecture
https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
https://en.wikipedia.org/wiki/Twin_prime#Twin_prime_conjecture
https://en.wikipedia.org/wiki/Fermat%27s_Last_Theorem

----

> [color=#f8a]
>
> 99. O teorema pequeno de Fermat.
> https://en.wikipedia.org/wiki/Euler%27s_theorem
> A função totiente de Euler.
> https://en.wikipedia.org/wiki/Euler%27s_totient_function
> O teorema de Euler.
> https://en.wikipedia.org/wiki/Euler%27s_theorem

### IDMb: Elementos da teoria dos números reais

1. Axiomas de corpo e suas primeiras consequências.
* unicidade da $(+)$-identidade ($0$)
* unicidade da $(·)$-identidade ($1$)
* leis de $(+)$-cancelamento
* unicidade dos $(+)$-inversos (opostos)
* $0$ é um $(\cdot)$-anulador: $0\cdot x = 0 = x\cdot 0$
* $-(-x) = x$
* $(-1)x = -x$
* $(-x)y = -(xy) = x(-y)$
* $(-x)(-y) = xy$
* leis de $(\cdot)$-cancelamento
* unicidade dos $(\cdot)$-inversos
* $xy=0 \implies x=0\ \text{ou}\ y=0$
1. Axiomas de corpo ordenado e suas primeiras consequências.
* $x > 0 \iff -x < 0$
* $x > 0\ \&\ y < z \implies xy < xz$
* $x < 0\ \&\ y < z \implies xy > xz$
* $x \neq 0 \implies x² > 0$
* $1 > 0$
* $0 < x < y \implies 0 < 1/y < 1/x$
* desigualdade triangular: $|x + y| ≤ |x| + |y|$
1. Representação geométrica.
* Intervalos
* Interpretação geométrica da expansão de um número real
1. Algumas noções métricas e topológicas da reta real
* a métrica euclidiana do ℝ
* ε-próximo; ε-vizinhança (ε-bola)
1. Subconjuntos notáveis do ℝ: N, Z, Q.
* O princípio da boa ordem
* O princípio da indução e indução forte
* O teorema binomial
1. Racionais e irracionais.
* Θ: Irracionalidade de √2
* Organização de demonstrações e uso de lemas
* Generalização sobre irracionalidades de outos números
1. Ínfimo, supremo, e o axioma da completude.
* Θ: Teorema de interseção de Cantor (intervalos aninhados)
* Θ: propriedade arquimediana dos reais
* Θ: densidade dos racionais nos reais
* Θ: existência de raizes
* um esboço da unicidade dos reais (unicidade de corpo orenado completo, a menos de isomorfismo)
1. Sequências, limites, e séries
* Θ: Unicidade de limite
* Θ: O teorema do confronto (sanduíche)
https://en.wikipedia.org/wiki/Squeeze_theorem
* Θ: Operações respeitadas pelo limite
* Θ: Toda sequência convergente é limitada
* Θ: Toda sequência convergente é Cauchy
* Θ: Toda sequência Cauchy é limitada
* Θ: Teorema da convergência monótona
https://en.wikipedia.org/wiki/Monotone_convergence_theorem
* Θ: Teorema de Bolzano--Weierstrass para os reais
https://en.wikipedia.org/wiki/Bolzano%E2%80%93Weierstrass_theorem
* Convergência e divergência de séries.
* O enunciado do teorema de rearranjo de Riemann.
https://en.wikipedia.org/wiki/Riemann_series_theorem
* O caso especial do teorema de interseção de Cantor para intervalos com diâmetros que tendem ao 0 e sua aplicação para a expansão de um número real em qualquer base $b > 1$.

----

## Objetivos de aprendizagem

### Comum

1. Familiarizar com a linguagem usada em definições e demonstrações matemáticas: aprender ler e escrever (usar e interpretar corretamente a linguagem matemática, sua nomenclatura e notação).
* axioma, teorema, corolário, lema, conjectura, definição, proposição, objeto, termo, variável
* notação de conjuntos e de funções
* «necessário e suficiente»
* «se e somente se»
* «proposição mais forte/fraca»
* «seja», «suponha»
* «generalização», «particularização»
* «sem perda de generalidade»
* «dualidade»
* «recíproca»
* «premissa»
* «hipótese»
* «contrapositiva»
* «pela escolha de»
* «eventualmente»
* «para valores suficientemente pequenos/grandes de»
* «determinado por», «caracterizado por»
* «existência e unicidade»
* «bem definido»
* «tende a»
* uso de artigo definido e indefinido
* «aquele ... tal que»
* declaração vs definição
1. Tipos e *type errors*; objetos vs proposições; igualdade vs equivalência lógica.
1. Apreciar a diferença entre intensional e extensional (sobre igualdades e equivalências).
1. Uso de (meta)variáveis em matemática; ocorrência de variável ligada vs livre; α-conversão (renomeamento); substituição de variável por termos; linguagem vs metalinguagem.
1. Introduzir o *lado computacional de uma demonstração, como sequência de comandos que alteram o estado de Dados/Alvo*.
1. Entender dois lados de matemática: intuitivo e formal.
1. Propriedades da igualdade e seu uso no raciocínio equacional.
1. Aprender como usar e escrever cálculos dentro de uma demonstração.
1. Apreciar a demonstração como justificativa da veracidade de proposições matemáticas (incluindo de proposições como $p\to p$, leis de distributividade, de De Morgan, frequentemente chamadas «leis» de lógica).
1. Aprender para cada um dos ¬,⇒,∨,∧,∃,∀: como introduzi-lo e como eliminá-lo *no texto de uma demonstração*.
1. Apreciar a lógica construtiva e os usos dos princípios da lógica clássica (terceiro excluído, redução ao absurdo, dupla negação, contrapositivo); apreciar a diferença entre redução ao absurdo e demonstração direta de negação.
1. Desenvolver definições e teorias matemáticas a partir de noções primitivas e axiomas.
1. Familiarizar com definições e demonstrações que envolvem conjuntos, sequências, funções, e relações.
1. Ter um primeiro contato com conjuntos estruturados e estruturas algébricas e as propriedades das suas operações.
1. Entender como e por quê os sistemas posicionais de numerais funcionam.

## Avaliação

A nota do aluno corresponde à avaliação dos seus textos matemáticos produzido nas provas avaliativas da disciplina, atendendo os pontos destacados no «Objetivos de aprendizagem».

*Sobre o uso recomendado de proof assistants:* optando para enriquecer sua metodologia nesta forma (onde o aluno desenvolve suas demonstrações escrevendo código), isso pode claramente valer pontos para o aluno mas sem permitir ao aluno passar escapando a produção de texto em *português matemático* corretamente escrito.

## Pointers

### IDMa

* Teoria dos números
* Criptografia
* Formalização de matemática
* Álgebra abstrata

### IDMb

* Análise real
* Formalização de matemática
* Algebra abstrata
* Espaços métricos
* Topologia geral
* Teoria dos conjuntos

## Bibliografia

### IDMa

* Birkhoff & Mac Lane (1977): *A Survey of Modern Algebra, 4th ed.* (Cap: 1)
* Pinter (1990): *A Book of Abstract Algebra, 2nd ed.* (Cap: 21, 22, 23)
* Mendelson (1973): *Number Systems and the Foundations of Analysis* (Cap: 3)
* Avigad, Lewis, van Doorn (2017): *[Logic and Proof][lean-lap]* (Cap. 19)

### IDMb

* Abbott (2015): *Understanding Analysis, 2nd ed.* (Cap: 1, 2, 4)
* Mendelson (1973): *Number Systems and the Foundations of Analysis* (Cap: 5)
* Rudin (1976): *Principles of Mathematical Analysis, 3rd ed.* (Cap: 1, 3)
* Tao (2016): *Analysis I, 3rd ed.* (Cap: 6,7,9)

### Comum & Auxiliar

* Munkres: *[Comments on Style][munkres-style]*
* Avigad, de Moura, Kong (2017): *[Theorem proving in Lean][lean-tpil]*
* Daepp, Gorkin (2011): *Reading, Writing, and Proving, 2nd ed.*
* Devlin (2012): *Introduction to Mathematical Thinking* (Cap: 4)
* Abbott (2015): *Understanding Analysis, 2nd ed.* (Cap: 3)
* Spivak (2008): *Calculus, 4th ed.* (Cap: 1)
* Tao (2016): *Analysis I, 3rd ed.* (Cap: B)

## Referências

* NNG: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
* Lean: https://leanprover-community.github.io/

----

[munkres-style]: https://tsouanas.org/teaching/docs/munkres-tips.pdf
[lean-lap]: https://leanprover.github.io/logic_and_proof/
[lean-tpil]: https://leanprover.github.io/theorem_proving_in_lean/