2022.2 FMC1, turma de Thanos

Horários de aula: 246N12 [18h45–20h25]
Sala A308
Contato:thanos@imd.ufrn.br
Playlists: FMC1 2022.2 (aulas gravadas)
FMC1 2019.1 (aulas gravadas)
Monitoria/TA: fmc.imd.ufrn.br
Turmas anteriores: ..

Info

Pré-requisitos

É pré-requisito desta disciplina ter aprendido o conteudo das disciplinas de matemática do primeiro semestre e (obviamente) do ensino médio também. Umas referências para esses conteudos 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.

¹ 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 os alunos matriculados têm 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

A disciplina FMC1 será dividida em 3 módulos–unidades. Podem considerar cada tal módulo como um componente curricular independente (e sem pré-requisitos entre si). Essa divisão é influenciada pelos módulos correspondentes à FMC1 baseados nos módulos correspondentes desta proposta.

IDMa: Elementos da teoria dos números inteiros

Axiomas sobre os inteiros (domínio de integridade bem ordenado). Demonstrações dos primeiros teoremas pelos axiomas, sobre as operações e as relações de ordem nos inteiros. A relação de divisibilidade e a verificação de suas principais propriedades. Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva. Lema de divisão de Euclides. Números, numerais, dígitos: demonstração que qualquer inteiro $b > 1$, serve como base para um sistema posicional de numerais para inteiros. Lema de Euclides e sua generalização. Teorema Fundamental da Aritmética. mdc e mmc e demonstrações das suas propriedades Algoritmo de Euclides: corretude e terminação Algoritmo estendido de Euclides Demonstração do teorema Fundamental de Aritmética Congruência módulo um inteiro e demonstrações das suas propriedades Aritmética modular e propriedades do ℤ/mℤ. Algumas conjecturas da teoria dos números: o teorema pequeno de Fermat; a função totiente de Euler; o teorema de Euler.

IRI: Introdução à Recursão e Indução

Os naturais e o tipo Nat; seus construtores (zero, sucessor) e sua teoria: implementação recursiva das suas principais operações, e verificação indutiva das suas principais propriedades. O tipo dos boolianos, Bool. Ordens sobre os naturais: especificação e verificação de suas propriedades. Outras funções e relações, e suas propriedades. Indução como princípio e técnica de demonstração em matemática. A unicidade dos naturais (a menos de isomorfismo). List Nat e List α: tipos de dados de listas: implementação recursiva e verificação indutiva de suas principais propriedades. Outros tipos de dados recursivos: tipos de árvores; tipos de expressões aritméticas; tipos de fórmulas; termos de cálculo-λ. Numerais binários, definição de semântica e seu uso para verificação de corretude.

IDMb: Elementos da teoria dos números reais

Axiomas de corpo e suas primeiras consequências. Axiomas de corpo ordenado e suas primeiras consequências. Representação geométrica. Algumas noções métricas e topológicas da reta real. Subconjuntos notáveis do ℝ: N, Z, Q. Racionais e irracionais. Conjuntos cotados, cota superior, cota inferior. Ínfimo, supremo. Seqüências e seus limites. O axioma da completude. Séries.

Objetivos de aprendizagem

IRI: Introdução à Recursão e Indução

Neste módulo estudamos como definir tipos de dados, funções, e relações recursivamente, e como demonstrar propriedades sobre tais coleções de dados por indução.

Prática com o uso da linguagem matemática e das principais técnicas de demonstração e refutação. Prática com a escrita de definições por recursão e demonstrações por indução. Recursão e indução estrutural sobre tipos de dados recursivos. Apreciação de coleções potencialmente infinitas do ponto de vista implementacional, recursivo, e verificação matemática de suas propriedades de interesse. Casamento de padrões e seu uso em definições, demonstrações, e cálculos. Recursão mútua, indução aninhada. Ganhar familiaridade com inferência de tipos e evitar erros de tipagem. Notação e nomenclatura matemática e computacional. Apreciar a diferença e a conexão entre sintaxe e semântica.

IDM: Introdução à Demonstração Matemática

Nestes módulos usamos elementos da teoria dos números inteiros (IDMa) e da teoria axiomática dos números reais (IDMb) 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)

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). Apreciar a diferença entre intensional e extensional (sobre igualdades e equivalências). 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. Introduzir o lado computacional de uma demonstração, como sequência de comandos que alteram o estado de Dados/Alvos. Entender dois lados de matemática: intuitivo e formal. Propriedades da igualdade e seu uso no raciocínio equacional. Aprender como usar e escrever cálculos dentro de uma demonstração. 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). Aprender para cada um dos ¬,⇒,∨,∧,∃,∀: como introduzi-lo e como eliminá-lo no texto de uma demonstração. 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. Desenvolver definições e teorias matemáticas a partir de noções primitivas e axiomas. Familiarizar com definições e demonstrações que envolvem conjuntos, sequências, funções, e relações. Ter um primeiro contato com conjuntos estruturados e estruturas algébricas e as propriedades das suas operações. Entender como e por quê os sistemas posicionais de numerais funcionam.

Bibliografia e referências

Conhece o libgen?

Principal

IRI: Introdução à Recursão e Indução

  • Mendelson (1973): Number Systems and the Foundations of Analysis (Cap. 2)
  • 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)
  • Steffen, Rüthing, Huth (2018): Mathematical Foundations of Advanced Informatics, vol 1 (Cap: 4, 5)
  • Bird & Wadler (1986): Introduction to Functional Programming (Cap. 5)
  • Hutton (2016): Programming in Haskell, 2nd ed.
  • Pierce et al.: Software Foundations, Vol 1 (Cap: Basics, Induction, Lists)
  • Fejer, Simovici (1991): Mathematical Foundations of Computer Science, Vol 1 (Cap. 4)

IDMa: Introdução à teoria dos números inteiros

  • Birkhoff & Mac Lane (1977): A Survey of Modern Algebra, 4th ed. (Cap: 1)
  • Mendelson (1973): Number Systems and the Foundations of Analysis (Cap: 3)
  • Avigad, Lewis, van Doorn (2017): Logic and Proof (Cap. 19)
  • Tao (2016): Analysis I, 3rd ed. (Cap: B1)
  • Dasgupta, Papadimitriou, Vazirani: Algorithms [DPV]

IDMb: Introdução à teoria dos números reais

  • 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,B2)

Comum & Auxiliar

  • Avigad, de Moura, Kong (2017): Theorem proving in Lean
  • Abbott (2015): Understanding Analysis, 2nd ed. (Cap: 3)
  • Daepp, Gorkin (2011): Reading, Writing, and Proving, 2nd ed.
  • Devlin (2012): Introduction to Mathematical Thinking (Cap: 4)
  • Spivak (2008): Calculus, 4th ed. (Cap: 1)

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

Obs.: As tecnologías/ferramentas seguintes podem mudar durante a disciplina—exceto a primeira. (Instalem e/ou criem uma conta para usar onde necessário.)

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

A parte IRI será auxiliada usando a linguagem de programação funcional Haskell e o proof assistant Lean. Usando uma linguagem de programação funcional é imediato implementar todas as suas definições para rodá-las no computador. Usando um proof assistant, formalizamos tanto as definições recursivas, quanto as demonstrações indutivas usando a mesma linguagem. (Mas o foco continua sendo o papel; não o computador!)

A parte IDMa será auxiliada pelo uso do proof assistant Lean.

A parte IDMb não será auxiliada por nenhum proof assistant. Ficará só no papel mesmo.

Regras

  1. Nunca escreva algo que você mesmo não sabe explicar: (i) o que significa; (ii) seu papel na tua resolução. Por exemplo: um aluno escreveu a frase seguinte na sua demonstração: «Como f é cancelável pela esquerda temos que g=h». Ele deve saber o que significa ser cancelável pela esquerda e também explicar como isso foi usado e/ou o que isso tem a ver com essa parte da sua demonstração.
  2. Qualquer trabalho poderá ser questionado em forma de prova oral, em modo privado ou aberto. Se um aluno não consegue explicar o que ele mesmo escreveu numa resolução, será considerado plágio (veja abaixo).
  3. Participando, nunca dê uma resposta que tu não pensou sozinho, exceto dando os créditos correspodentes.
  4. Não tente “forçar a barra” perguntando ou respondendo coisas aleatórias com objetivo único de ganhar pontos. Os pontos de participação não correspondem em apenas perguntas ou dúvidas que mostram interesse. O interesse é implícito pelo fato que tu escolheu matricular nesta turma—não vale pontos.
  5. Não procurem resoluções em qualquer lugar fora dos indicados em cada homework. O único recurso aceitável para procurar ajuda é no nosso Zulip (especificamente seus canáis públicos—não DM) e a monitoria.
  6. Proibido consultar o apêndice de resoluções do fmcbook durante a disciplina exceto quando for explicitamente permitido por mim. (Os apêndices de dicas são permitidos sim.)

Uns deveres dos alunos

  1. Visitar o site e o Zulip da disciplina pelo menos uma vez por dia durante o semestre. (Qualquer coisa postada no site ou no Zulip da disciplina será considerada como conhecida por todos os alunos da turma.)
  2. Estudar o conteúdo lecionado e tentar resolver todos os trabalhos atribuidos.
  3. Participar no Zulip diariamente, compartilhando tuas resoluções para receber feedback, e checando as resoluções de outros colegas para dar feedback.
  4. Checar e atender seu email cadastrado no SIGAA pelo menos uma vez por dia durante o semestre.
  5. Participar nas aulas! Obs.: tendo uma dúvida durante a aula, levante a mão para solicitar “a fala” e assim que a receber, pergunte! Não espere o fim da aula para discutir tua dúvida em “modo particular”! A maioria das vezes eu vou negar isso e pedir ao aluno iniciar a discussão no Zulip ou na próxima aula.
  6. Participar nas aulas de exercícios de monitoria e utilizar seus horários de tirar dúvidas.

(Veja também os FAQs relevantes.)

Sobre plágio

  1. Plágio detectado implica que o aluno será reprovado imediatamente por nota e por faltas.
  2. Entregar tuas resoluções para um aluno copiar é proibido do mesmo jeito, e também não ajuda mesmo ninguém.

Cadernos vs. celulares

Não faz sentido aparecer na aula sem caderno. E não faz sentido aparecer na aula com celular ligado; bote no modo avião antes de entrar na sala. As aulas são interativas e se não pretende participar e concentrar nesses 100 minutos, sugiro ficar fora e escolher uma outra maneira de passar teu tempo. Não é necessário (e obviamente nem suficiente) aparecer nas minhas aulas para passar.

Avaliação e faltas

Disclaimer. Eu suponho que os alunos desta turma escolheram se matricular por interesse em aprender seu conteúdo. O ideal seria ignorar assuntos irrelevantes de avaliação, presenças, carga horária, etc., e se jogar nos estudos.

Avaliação

A nota final de cada aluno vai ser principalmente baseada em um ou mais dos: (i) provas escritas; (ii) sua participação; (iii) trabalhos atribuidos; (iv) hw resolvidos (veja o FAQ relevante).

Cada aluno será responsável para manter organizado e bem escrito o seu caderno com todos os teoremas e exercícios que estudou durante a disciplina.

Presenças e faltas

A presença pela regulação da UFRN é obrigatória. Os alunos que não gostam/querem/podem aparecer nas minhas aulas ainda tem chances de ganhar até nota máxima e aprovar na disciplina. Ou seja: alunos que escolhem não participar ou aparecer nas aulas, e mesmo assim aparecem nas provas escritas e conseguem nota final de aprovação vão ter sua porcentagem de faltas ajustada para não reprovar por faltas. Esclarecimento: alunos que não conseguem nota final de aprovação não terão sua porcentagem de presença ajustada de jeito nenhum e por nenhum motivo.

Obviamente, alunos que não aparecem nas aula não terão como ganhar pontos de participação—duh!—nem acesso nos pontos de possíveis provas-surpresas.

As presenças/faltas serão cadastradas usando o sistema Plickers (veja o FAQ relevante).

Atrasados

Definição (atrasado). Seja $a$ aluno desta turma. Dizemos que $a$ é atrasado sse $a$ não está já sentado na sua mesa, com seu caderno já aberto, seu celular já desligado e na mochila, no momento que a aula começa.

Tentem estar presentes na sala da aula ANTES do horário do seu começo, e fiquem até o fim da aula.

Caso que alguém chega atrasado: não faz sentido bater na porta da sala de aula; não faz sentido cumprimentar nem o professor (não é mostra educação cumprimentar nesse caso—pelo contrário!) nem os amigos/colegas da aula. Entrando numa sala onde a aula já começou, tentem fazer sua entrada o menos possível notada por os participantes pois atrapalha a concentração de todos.

FAQs

Dynamic content

Pontos de participação

Provas

Provas surpresa. Note que em qualquer aula pode ter prova surpresa, cujos pontos são considerados «pontos extra», assim sendo possível tirar nota máxima (100), mesmo perdendo todas as provas surpresas.

U1 (IDMa)

U2 (IRI)

U3 (IDMb)

Homework (HW)

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.

2022-08-23

  1. Capítulo 1.

2022-08-25

  1. Complete o «Tutorial World» do Natural Number Game. Veja o FAQ relevante também.
  2. Capítulo 3.

2022-08-25

  1. Demonstre o 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.

2022-08-29

  1. Para cada uma das proposições acima 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)]
  2. Demonstre os teoreams em cima 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!

2022-09-02

  1. Cap «Os inteiros», «§. Primeiros passos»
  2. Demonstre os teoremas seguintes sobre os inteiros a partir dos axiomas (procure esclarecimentos no Zulip). Tome cuidado com umas das quantificações que deixei implicitas.
    1. unicidade da $(+)$-identidade (0)
    2. unicidade da $(⋅)$-identidade (1)
    3. leis de $(+)$-cancelamento
    4. unicidade dos $(+)$-inversos (opostos)
    5. 0 é um $(⋅)$-anulador: $0⋅x = 0 = x⋅0$
    6. $-(-x) = x$
    7. $(-1)x = -x$
    8. $(-x)y = -(xy) = x(-y)$
    9. $(-x)(-y) = xy$
    10. leis de $(⋅)$-cancelamento
    11. (|) é reflexiva: (∀a)[a | a]
    12. (|) é transitiva: (∀a,b,c)[a | b & b | c ⇒ a | c]
    13. qualquer inteiro divide o 0
    14. tem inteiros que o 0 divide?
    15. os $1$ e $-1$ dividem qualquer inteiro?
    16. d | a & d | b ⇒ d | ax + by
    17. a | b & b | a ⇒ a = b ?

2022-09-06

  1. Cap «Os inteiros», até «§. Conjuntos fechados sobre operações»
  2. Demonstre, ainda com os 8 primeiros axiomas (4 aditivos, 3 multiplicativos, e a distributividade) a equivalência entre:
    • (Z-NZD): (∀a,b)[ ab = 0 ⇒ a = 0 ou b = 0 ]
    • (Z-LC): (∀a,b,c)[ ca = cb ⇒ c = 0 ou a = b ]

2022-09-09

  1. Demonstre que as duas abordagens vistas na aula são equivalentes:
    • (ℤ;0,1,+,-,·,<) + (ZO-Trans) + (ZO-A) + (ZO-M) + (ZO-Tri)
    • (ℤ;0,1,+,-,·,Pos) + (ZP-ACl) + (ZP-MCl) + (ZP-Tri)
  2. Cap «Os inteiros», até «§. Ordem e positividade»

2022-09-12

  1. Considere os inteiros das peimeiras aulas, até a especificação (2/5).
    1. Demonstre que o 0≠1 não é demonstrável a partir desses axiomas.
  2. Considere o (A; ♡, κ) com a especificação seguinte, e demonstre que não tem como demonstrar a Comutatividade de (♡), nem como refutá-la.
    • (♡) : A × A → A
    • κ : A
    • (Ass) : (∀a,b,c)[ (a ♡ b) ♡ c = a ♡ (b ♡ c) ]
    • (IdR) : (∀a)[ a ♡ κ = a ]

2022-09-15

  1. Até o «§. Valor absoluto»
  2. Π4.1, Π4.2, Π4.3, Π4.4

2022-09-16

  1. Usando o princípio da boa ordem (qualquer conjunto não vazio de inteiros positivos possui mínimo) demonstre: não existe inteiro $c$ tal que $0 < c < 1$.
  2. O «não vazio» acima é redundante?
  3. Demonstre que um conjunto vazio é subconjunto de qualquer conjunto.
  4. Demonstre ou refute: «o Ø é bem-ordenado».
  5. Até o primeiro intervalo de problemas.
  6. Demonstre ou refute: «qualquer conjunto de inteiros X finito é bem ordenado».
  7. Escreva os comandos que temos sobre ataques e usos dos conectivos (∧),(∨),(⇒) como regras de inferência.
  8. Demonstre como teorema o princípio da indução.
  9. Demonstre como corolário o princípio da indução com 2 bases.

2022-09-23

  1. Resolva em condições de prova as provas seguintes:
    1. Prova 2.X de 2019.2
    2. Prova 2.Y de 2019.2
    3. Prova 2.Z de 2019.2
  2. Resolva em condições tranqüilas as mesmas provas.

2022-09-26

  1. Escreva sozinho a definição de m.d.c.
  2. Troque o que precisa trocar para virar a definição de mínimo.
  3. Troque o que precisa trocar para virar a definição de máximo.
  4. Troque o que precisa trocar para virar a definição de m.m.c.
  5. Dados inteiros a,b, demonstre a existência dum m.d.c. deles, e mostre que ele pode ser escrito como combinação linear dos a,b.
  6. Demonstre as propriedades básicas dum m.d.c., que denotamos aqui simplesmente por (_,_), exceto uma, que é refutável (e logo refute e depois obviamente tente a ajustar para virar demonstrável, e demonstre–phew!):
    1. (a,b) = (a,-b) = (-a,b) = (-a,-b)
    2. (a,a) = ?
    3. (a,0) = ?
    4. (a,1) = ?
    5. (a,b) = (b,a)
    6. ((a,b),c) = ?
    7. (a,b) = (a, a + b)
    8. (a,b) = (a, a - b)
    9. (ca,cb) = c(a,b)
    10. (uv,a) = (u,a)(v,a)
    11. (a,b) = (b, rem(a,b))
  7. Demonstre: Invertible(x) ⇔ Unit(x)
  8. Demonstre: Irreducible(x) ⇔ Prime(x)
  9. Demonstre ou refute: apra quaisquer primos distintos p,q, pq | n² ⇒ pq | n.
  10. 🚀 Bora viajar legal!
    1. Num universo de conjuntos (por exemplo no Set(Int)) considere a mesma definição de m.d.c., mas essa vez usando como guia a ordem de (⊆). Qual conceito definiu? O que acontece se virar as direções? (⊇).
    2. Tendo P, Q : Prop, escrevemos P ⊢ Q para a (meta)proposição «Dado a P, podemos demonstrar a Q.». No universo de proposições, mostre que (⊢) é uma pré-ordem. Qual seria o “m.d.c.” de duas props, e qual o “m.m.c” delas?

2022-09-28

  1. Troque o (Z-PBO) pelo princípio da indução (Z-Ind). Demonstre o (Z-PBO).

2022-09-29

  1. 💻 Na aula foi óbvio que ninguém merece fazer contas na mão, mesmo utilizando um algoritmo eficiente. Mas somos programadores—right?—e logo: programe na tua linguagem favorita uma função que dados dois inteiros a, b, retorna seu m.d.c. d, e também coeficientes Bézout x,y tais que d = ax + by. Dica: caso que tua linguagem favorita não seja a Haskell, troque e tente novamente.
  2. L: a ≥ b > 0 ⇒ r < a/2. (Aqui a/2 é o quot(a,2).)
  3. Θ: Para todo n ≥ 1, e quaisquer inteiros a > b > 0, se o algoritmo de Euclide precisa n passos (divisões) para terminar, então a ≥ fib(n+2) e b ≥ fib(n+1), onde fib(i) é o i-ésimo número Fibonacci.

Histórico

2022-08-22: Aula 01: Overview; tipos [video]

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

2022-08-24: Aula 02: 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,∀,∃,=

2022-08-26: Aula 03: 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

2022-08-29: Aula 04: 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

2022-08-31: Prova 1.1

2022-09-02: Aula 05: Demonstrações; Os inteiros (1) [video]

Demonstrações

  • 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

IDMa: Os inteiros (1)

  • Especificação × Implementação
  • Os inteiros $(\mathbb Z;0,1,+,-,\cdot)$
  • Axiomas sobre os inteiros
  • Axiomas vs Teoremas

2022-09-05: Aula 06: Os inteiros (2) [video]

  • bom dia / recap
  • Teoremas x axiomas; dependências de demonstrações
  • Q: por que não aparece (=) na estrutura dos inteiros?
  • Q: como rotular teoremas?
  • Sintaxe vs Semântica; convenções sintácticas
  • juxtaposição; notação infixa/postfixa/prefixa
  • arvore sintáctica; parsing; precedência sintáctica de operadores
  • associatividade sintáctica
  • Operações primitivas vs. definidas
  • subtração como operação definida e não primitiva
  • uns numerais para ajudar: 2, 3, …
  • potências com expoentes naturais; convenção sobre associatividade sintáctica da exponenciação
  • Q: igualdade sintáctica vs intensional
  • Q: o parsing se trata de quais operações?
  • Cancelamento multiplicativo
  • Q: qual a associatividade sintáctica da (⇒)?
  • Q: refutação..?
  • Não-zerodivisores.
  • Q: o «ou» é exclusivo?
  • (Plicker) axiomas ou teoremas?
  • A resposta certa; mais teoremas
  • Existência e unicidade; artigo indefinido vs definido; proof by fight club; alternativa conhecendo já um legal

2022-09-09: Aula 07: Os inteiros (3) [video]

  • Dica sobre como enxergar alvos
  • A utilidade de lemmas sobre unicidade de resolução de equações num incógnito
  • Exemplos: (∀a)[(-1)a = -a]; (∀a)[0a = a]
  • Axioma x Teorema; Noção primitiva x definida
  • Axiomas sobre ordem: duas maneiras de axiomatizar
  • A (≤) nos naturais é definível
  • Conjunto fechado sob operação
  • Notação set-builder (com comprehension)
  • interpretação de (∈)
  • Como tratar um subconjunto como predicado unário
  • 1 é positivo: teorema ou axioma?
  • O módulo (absolute value) |_| : Int → Int
  • Para refletir: a independência duma proposição: indemonstrabilidade e irrefutabilidade

2022-09-12: Aula 08: Os inteiros (4) [video]

  • como definir «ser fechado sob uma operação n-ária (para n=1,2)
  • uma primeira conversa “adulta” sobre conjuntos
  • um preconceito sobre as () na notação f(x)
  • a notação set-builder: como ler e escrever, e como não ler e como não escrever
  • O que significa «_ ∈ { 3x | x ∈ ℤ }»
  • A diferença intensional entre os extensionalmente iguais conjuntos: {x ∈ A | x ∈ B} e {x ∈ B | x ∈ A}
  • o 3ℤ é fechado sob adição e subtração
  • como generalizar para o mℤ
  • Θ. 1 é positivo
  • Como demonstrar a indemonstrabilidade de proposições
  • A indemonstrabilidade do 0 ≠ 1
  • notação infixa x postfixa x prefixa x mixfixa

2022-09-14: Aula 09: Os inteiros (5) [video]

  • Não existe inteiro estritamente entre 0 e 1: teorema ou axioma?
  • Como escrever definições
  • Duas maneiras que uma definição pode ser errada
  • Quando precisamos demonstrar algo para justificar uma definição ou uma notação
  • o mínimo dum conjunto, quando existe é único
  • Umas propriedades do valor absoluto

2022-09-16: Os inteiros (6) [video]

  • um pleno «tal que» é capaz de destruir uma frase e torná-la pior-que-errada
  • Princípio da boa ordem ($\mathbb Z_{>0}$ é bem ordenado)
  • Como usar o PBO na prática
  • Principios de indução como teoremas
  • Princípio da indução para os inteiros: se $S$ é (+1)-fechado e $1 \in S$, então $\mathbb Z_{>0} \subseteq S$
  • Outras versões de PBO e de Indução e como obtê-las “hackeando” as originais
  • Indução com mais que uma base

2022-09-19: Os inteiros (7) [video]

  • uma interpretação geométrica dos inteiros
  • PBO shiftado e demais versões
  • Indução forte (“course-of-values”)
  • Quebrando os inteiros em tijolinhos atômicos usando como cimento: (i) adição; (ii) multiplicação
  • Definição de invertível
  • Definição de irredutível

2022-09-21: Os inteiros (8) [video]

  • O que queremos? (Wishlist)
    • Divisão (quot e rem)
    • algoritmo para calcular os quot e rem
    • definir e justificar sistemas posicionais de numerais
    • mdc e mmc
    • fatorização única (ao menos de coisas sensatas) de inteiros (teorema fundamental de aritmética)
  • O lemma da divisão de Euclides: enunciado
  • Números, numerais, dígitos
  • Expansão e sistemas posicionais
  • Notação Σ de somatórios
  • O logaritmo como tamanho de númerais melhor que o length deles como strings
  • Enunciado do Teorema Fundamental de Aritmética (fatorização única)
  • Explicação intuitiva sobre como sistemas posicionais funcionam
  • generalização da palavra “maior” para outras ordens
  • diagrama Hasse para os $\mathbb{Z}_{\geq 0}$
  • mdc: definição nível coração

2022-09-23: Os inteiros (9) [video]

  • O lemma da divisão de Euclides: esboço de demonstração
  • Esboço de demonstração do teorema dos sistemas posicionais (expansão em base $b$): qualquer inteiro $b>1$ serve como base para um sistema posicional de numerais para inteiros.
  • “mℤ” ⇔ “fechado sob ops”: concretização e esboço
  • Duas maneiras de obter membros arbitrários de um conjunto indexado
  • Esboço do Teorema Fundamental de Aritmética (fatorização única de inteiros)

2022-09-26: Os inteiros (10) [video]

  • Invertible, Unit, Irreducible
  • Prime
  • m.d.c.
  • Um exemplo: m.d.c. dos 12,18; divs; comdivs
  • Q: como assim um-maior? A: hmm-maior
  • O que acontece se trocar de (|) para (≤)?
  • O que acontece se trocar de direção nas ordens?
  • Q: qual o tipo desse min?
  • Dados a,b, existe mesmo um m.d.c. deles?
  • Como vou escolher o m.d.c. se os comdivs são esses?
  • Θ. Existência de m.d.c.
  • Q: qual o nome da alma que os m.d.c. e o min compartilham?
  • Duas maneiras de obter membro arbitrário de conjunto indexado
  • Q: Como exatamente funciona essa notação set builder?
  • m.d.c. vs m.m.c (teaser de dualidade)
  • mesmo demonstrando a existência, queremos algoritmo e de preferência eficiente

2022-09-28: Prova 1.3; Os inteiros (11) [video]

  • Como demonstrar (a,b)=(c,d).
  • Algoritmo de Euclides: corretude e terminação
  • Terminação, Corretude, Eficiência
  • Algoritmo estendido de Euclides
  • coprimos

Futuro (fluido)

2022-09-30: Os inteiros (12)

  • Algo que parece LEM, mas não é
  • Lema de Euclides e sua generalização
  • Dum lemma para uma ideia: n² (im)par ⇔ n (im)par
  • “unicidade” de m.d.c.
  • Teorema de Euclides sobre infinidade de primos e sua demonstração construtiva
  • Densidade de primos e gaps
  • Conjecturas
  • Congruência módulo um inteiro e demonstrações das suas propriedades
  • Aritmética modular e propriedades do $\mathbb Z / m\mathbb Z$
  • (·)-inversos módulo um inteiro m
  • Invertibilidade módulo $m$
  • Unicidade de inverso módulo $m$ e o que significa
  • Uns casos extremos: módulo 1, módulo 0
  • Algumas conjecturas da teoria dos números
  • Sistemas de resíduos
  • De Fermat para Euler

2022-10-05: Os inteiros (13)

  • Mais Euler

2022-10-07: Os inteiros (14)

  • Criptografia

2022-10-10: Prova 1.4; Recursão, Indução (1): Nat

2022-10-14: Recursão, Indução (2)

2022-10-17: Recursão, Indução (2)

2022-10-19: Recursão, Indução (3)

2022-10-21: Recursão, Indução (4)

2022-10-24: Recursão, Indução (5)

2022-10-26: Recursão, Indução (6)

2022-10-31: Recursão, Indução (7)

2022-11-04: Recursão, Indução (8)

2022-11-07: Recursão, Indução (9)

2022-11-09: Recursão, Indução (10)

2022-11-11: Recursão, Indução (11)


2022-11-14: Os reais (1)

2022-11-16: Os reais (2)

2022-11-18: Os reais (3)

2022-11-23: Os reais (4)

2022-11-25: Os reais (5)

2022-11-28: Os reais (6)

2022-11-30: Os reais (7)

2022-12-02: Os reais (8)

2022-12-05: Os reais (9)

2022-12-07: Os reais (10)

2022-12-09: Os reais (11)

2022-12-12: Os reais (12)

2022-12-14: Os reais (13)

2022-12-16: Os reais (14)

2022-12-19

2022-12-21

2022-12-23

Last update: Thu Sep 29 10:20:41 -03 2022