2019.1 FMC2, turmas de Thanos

Horários: 246T34 [14h55–16h35] @ A308 (U1; U2)
246N12 [18h45–20h25] @ A308 (U1; U2; U3)
Sala do prof:A225
Contato:thanos@imd.ufrn.br
Aulas gravadas: 2019.1; 2018.2
Study group: Telegram, atraves de link disponível em notícia do SIGAA [regras]
Monitoria/TA:fmc.imd.ufrn.br
Horário de atendimento:mande email para marcar (tente primeiro discutir tua dúvida no study group, e na monitoria)
Turmas anteriores: 2018.2; 2018.1; 2017.2; 2017.1; 2016.1

Prerequisitos

É prerequisito ter aprendido bem o conteudo transversal de FMC1. Sem aprender esses assuntos primeiro, não faz sentido se matricular em FMC2. (Obs.: aprenderpassar.)

Então—ANTES de começar—é bom estudar os:

  1. How to prove it, de Velleman (1, 2, 3)
  2. Do fmcbook os capítulos:
    • Linguagens
    • Demonstrações
    • Os números naturais: recusão; indução
    • Combinatória enumerativa
    • Teoria elementar de números
    • Congrüências
  3. Mathematical Proofs, de Chartrand, Polimeni, Zhang (0, 2)
  4. Comments on style de James Munkres.
  5. A parte “Writing mathematics” do livro The tools of mathematical reasoning, de Lakins.

(Obs.: estudarler.)

Conteúdo

Conteúdo transversal (durante todas as unidades)
Lógica proposicional e de predicados (linguagem; sintaxe e semântica). Definições e provas. Demonstrações diretas e indiretas, refutações. Definições por recursão – provas por indução. A linguagem de conjuntos, funções, e relações.
Linguagem; Lógica; Recursão; Indução (U0)
Crash course!
Conjuntos, Funções, e Relações (U1)
Conjuntos, sua notação, suas operações, e seus leis. Uniões disjuntas, famílias e partições. Tuplas ordenadas e produto cartesiano. As operações unitárias de união e interseção. As relações de subconjunto, e de pertencer. Multiconjuntos e sequências. Funções, o conceito de função e suas propriedades. Intensão x extensão. Domínio, codomínio. Imagem, pre-imagem. Funções totais e parciais, injetivas, sobrejetivas, bijetivas. Aridade. Função constante, função identidade, projeções, funções características. Funções recursivas; recursão mutual. Funções de ordem superior. A notação de λ-calculus. Funções x predicados. Relações e suas propriedades. Relações de equivalência, clásses de equivalência. Operações em relações, inversão, composição, fechos.
Elementos de Álgebra abstrata (U2)
Conjuntos com estrutura. Operações. Teoria dos grupos. Demonstrações com o uso de identidades algébricas. Homomorfísmos. Outras estruturas: aneis, monoides, reticulados. Álgebras booleanas.
Elementos de Teoria de Conjuntos (U3)
Enumerações e conceito intuitivo de cardinalidade. Paradoxos e os axiomas Zermelo–Fraenkel. Representações de matemática (traduções). Os números naturais; axiomas Peano.
Elementos de Teoria de Ordem (U3)
Ordens parciais, totais, densas, bem-fundadas. Diagramas de Hasse. Elementos notáveis (majorantes, máximos, supremos). Conjuntos ordenados, reticulados, reticulados completos. Construções de conjutos ordenados. Dualidade. Ordens canônicas, ordens lexicográficas. Monotonicidade. Teoremas de ponto fixo. Conjuntos bem-ordenados.
Aplicações e assuntos auxiliares
Relações bem-fundadas e indução transfinita. Números ordinais. Limites de computação. Noções de decidibilidade e de semi-decidibilidade. λ-calculus, lógica combinatória. Elementos de teoria dos tipos. Noções de semántica de linguagens de programação. Y-combinator, fixpoints e recursão. Axiom of choice e suas conseqüências. Tipos de dados algébricos. Programação funcional. Programação lógica. Bancos de dados.

Bibliografia

(Conhece o libgen.io?)

Principal

Auxiliar

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

  • Pierce et al: Software Foundations, Volume 1: Logical Foundations [SF1]
  • Lawvere & Schanuel: Conceptual Mathematics: A first introduction to categories (I, II)
  • Velleman: How to prove it (1–3)
  • Pinter: A book of abstract algebra (2–5, 6, 12, 17)
  • Davey & Priestley: Introduction to lattices and order (1, 2) [DP]
  • Paul Halmos: Naïve set theory
  • Moschovakis: Notes on set theory (1, 2, 3–5, 6–7) [NST]
  • Goldrei: Classic set theory, for guided independent study (4, 7, 8)
  • Raymond Smullyan: Satan, Cantor, and Infinity
  • Raymond Smullyan: A beginner's guide to mathematical logic (Volume 1)
  • Paul Halmos: Linear Algebra Problem Book (1)
  • Birkhoff & Mac Lane: A survey of modern algebra (1.11; 1.1–1.5, 1.10, 1.12)
  • Aluffi: Algebra: Chapter 0
  • Mac Lane & Birkhoff: Algebra (1.1–1.3)
  • Herstein: Topics in Algebra (2.1–2.5 [skip # and *])
  • Simmons: Introduction to topology and modern analysis (1)
  • Munkres: Topology (1)
  • Loomis & Sternberg: Advanced Calculus (0)
  • João Marcos: Lógica Aplicada à Computação website (TdC, R&I)

Programação

Links

Dicas

Avaliação

Pontos

A disciplina é dividida em 3 unidades (vejá Conteudo). Em cada unidade o aluno vai receber de 0 a 100 pontos. As provas escritas de cada unidade terão 100 pontos em total. (Para pegar uma idéia dessas provas, olhe nos sites das minhas turmas de FMC2 de semestres passados.)

Alem desses pontos, um aluno pode ganhar pontos extra: por participação; por homework; ou por provas-surpresas. Esses pontos valem igualmente com os pontos de prova escrita. Estou tenando ao máximo ser justo com esses pontos, mas nenhuma justificativa será dada por ganhar (ou não ganhar, ou perder!) pontos extra.

Umas regras: (1) nunca dê uma resposta que tu não pensou sozinho; (2) não tente “forçar a barra” dando respostas aleatórias nas minhas perguntas com objetivo único de ganhar pontos extra.

Umas provas escritas podem ter pontos bônus. Esses são pontos que são condicionalmente considerados: para considerá-los um aluno precisa ter pelo menos 50pts normais (não-bônus). As questões que valem pontos-bônus são em geral em assuntos auxiliares que, mesmo que merecem ser reconhecidos, não devem ser determinantes para aprovar na disciplina.

Presenças

Veja notícia no SIGAA para informações sobre presenças, chamadas, plickers, etc.

Provas

As provas principais serão avisadas com antecedência de pelo menos 48 horas.

Provinha 0

  • Provinha 0 (pts: 0; bônus: 0) (dia: 16/02/2019)
    { uncensored, answers }
    correções: p1 (8M), p2 (5M).

Unidade 1

Unidade 2

Unidade 3

Reposição

  • Prova 4 (pts: 100; bônus: 0) (dia: 26/06/2019)

Homework

Obs.:

  • Estudar um assunto dum livro obviamente inclui resolver todos os exercícios e problemas.
  • «Até» é sempre inclusivo.
  • Homeworks marcados assim são opcionais; considero o resto obrigatório.
  • Depois de cada aula, um homework é sempre válido, obrigatório, e essencial: sem olhar para teu caderno, defina todas as noções e demonstre TODOS os teoremas da aula;
    while (não conseguiu) {
      estude o assunto;
      tente novamente;
    }
    

09/01/2019

  1. Estude os ítens que tenho nos prerequisitos.
  2. Brinque com Haskell ou PureScript.
  3. Estude a (pouca) coisa que tá escrita no capítulo «Estratégias de provas» do fmcbook.
  4. Estude e resolve os exercícios/problemas do capítulo 3 de Velleman.
  5. Estude o capítulo «Linguagens» do fmcbook.
  6. Estude o capítulo «A linguagem de lógica proposicional» do fmcbook.
  7. Estude os capítulos 1–2 de Velleman.
  8. Estude brutalmente o capítulo «Os números naturais: recursão; indução» do fmcbook, e assista minhas aulas relevantes do FMC2/2018.2 (as 3 primeiras aulas).
  9. Installe o Coq; dê uma lida no «Preface» do SF1 (link na Bibliografia); estude o capítulo «Basics» do SF1.

04/02/2019

  1. Estude as «Prova 0» dos semestres passados (2017.1; 2017.2; 2018.1; 2018.2). Tente resolvê-las sozinho. Depois, leia bem todas as correções digitalizadas dos alunos dos semestres anteriores, para aproveitar dos comentários disponíveis. (Melhor estudar isso «por página».)

13/02/2019

  1. Estude as poucas coisas que estão escritas no Capítulo I
  2. Capítulo 3: até §24
  3. Problemas: Π3.1–Π3.5.

16/02/2019

  1. Capítulo 3
  2. Capítulos 4–5

18/02/2019

  1. Capítulo 6: até §38

21/02/2019

  1. Faça finalmente o hw #9 do dia 09/01/2019!
  2. Faça finalmente o hw #8 do dia 09/01/2019!

23/02/2019

  1. Brinque com: Haskell; PureScript; ou Idris (lembra do hw #2 do dia 09/01/2019?)
  2. Numa das linguagens funcionais acima, implementa (você mesmo) o tipo de naturais, e defina a adição, multiplicação, e exponenciação
  3. Estude o capítulo «Proof by induction» do [SF1]
  4. Capítulo 11: estude bem e resolva todos os exercícios
  5. Problemas: Π11.1

24/02/2019

  1. Estude todas as correções da Prova 0

25/02/2019

  1. Problemas: Π11.2; Π11.3
  2. Problema: Π11.4

27/02/2019

  1. Estude as §§55–58 (cap. 7)
  2. Problemas: Π7.1; Π7.2; Π7.3; Π7.5; Π7.6
  3. Problemas: Π7.7; Π7.8; Π7.9
  4. Estude as §§104–106,109

01/03/2019

  1. Estude as §§104–113

08/03/2019

  1. Estude as §§114–116
  2. Problemas: Π12.1; Π12.2; Π12.3; Π12.8; Π12.9

11/03/2019

  1. Estude as §§114–124
  2. Problemas: Π12.4; Π12.5; Π12.6; Π12.7; Π12.10; Π12.11; Π12.12; Π12.13
  3. Problemas: Π12.14
  4. Defina recursivamente o somatório e produtório finito (bounded) duma seqüência {aₙ}ₙ

13/03/2019

  1. Estude as §§125–128

14/03/2019

  1. Assista a aula correspondente do 2018.2 para esclarecer a resolução dos Π12.11–12
  2. Comece estudar os Parts I & II do [Lawvere]

15/03/2019

  1. Estude as §§129–130

18/03/2019

  1. Estude as §§131–135

19/03/2019

  1. Re-estude a §130

20/03/2019

  1. Estude as §§136–137
  2. Problemas: Π13.1; Π13.2; Π13.3; Π13.4; Π13.5; Π13.9; Π13.10; Π13.11

21/03/2019

  1. Re-estude a §137
  2. Problemas: Π13.1; Π13.2; Π13.3; Π13.4; Π13.5; Π13.6; Π13.7; Π13.8

22/03/2019

  1. Re-estude a §136, especialmente as iterações
  2. Estude a §138

25/03/2019

  1. Resolva as atividades das secções instáveis mencionadas abaixo (especialmente todas as equivalências da «viagem épica»)
    AVISO: as secções «Uma viagem épica», «Estilo pointfree» não são estaveis no fmcbook; os assuntos são auxiliares; mas as atividades que aparecem lá são muita boa prática para os assuntos não-auxiliares!
  2. Estude as secções «Imagens; preimagens» e «Funções de ordem superior»
  3. Problemas: Π13.9; Π13.10; Π13.11; Π13.12; Π13.13; Π13.14

26/03/2019

  1. Problemas: Π13.9; Π13.10; Π13.11; Π13.12; Π13.13; Π13.14; Π13.15; Π13.19; Π13.20

27/03/2019

  1. Secções: «Funções parciais»; «Currificação»; «Fixpoint»; «Conjuntos indexados e famílias indexadas»; «Definições recursivas» [até o item «O que tá acontecendo?»]
  2. Problemas: Todos exceto o que se trata da «(FIB)»
  3. Resolva finalmente o hw do dia 21/03/2019, especialmente o Π13.8

30/03/2019

  1. Resolva todos os problemas das provas 1.1T, 1.1N, 1.2T, 1.2N
  2. Estude os gabaritos
  3. Estude a secção «Definições recursivas» inteira
  4. Estude a secção «Conjuntos indexados vs. famílias indexadas» do capítulo 12

03/04/2019

  1. Estude o Capítulo 15 até a §154

05/04/2019

  1. Estude as §§155–158
  2. Problemas: todos do primeiro intervalo de problemas

08/04/2019

  1. Estude a §159 «Relações de ordem»
  2. Estude as §§161–162
  3. Estude as §§163–164
  4. Problemas: todos os problemas do Capítulo 15 excéto o último
  5. Problemas: o último

11/04/2019

  1. Leia o artigo Revenge of the nerds, de Paul Graham
  2. Brinque com Haskell/PureScript/Agda/Idris, usando as idéias que temos encontrado na Unidade 1
  3. Conheça uma LISP: Racket e/ou Clojure
  4. Para programadores de Java, C++, e C#: palestra introduzindo Scala por Venkat Subramaniam

12/04/2019

  1. Estude o Capítulo 17
  2. Estude o Capítulo 18 até a §171

15/04/2019

  1. §172
  2. Problemas: Π18.1; Π18.2; Π18.3

16/04/2019

  1. Problemas: Π18.1; Π18.2; Π18.3; Π18.4

17/04/2019

  1. Resolva todo o homework que tu tem deixado pra lá
  2. §§173–175 até o Exercício x18.47 até o x18.49
  3. §121: «Conjuntos indexados vs. famílias indexadas»

22/04/2019

  1. §§175–176
  2. Problemas: Π18.8; Π18.9

24/04/2019

  1. Teorema: intersecção de família de subgrupos é subgrupo
  2. Lema: Ha = H ⇔ a ∈ H
  3. Conseqüência: a ∉ H ⇔ Ha ≠ H
  4. Lema: a ∉ H ⇔ Ha, H disjuntos
  5. Para quais a∈G, temos Ha ≤ G?
  6. Lema: todas as coclasses direitas têm a mesma cardinalidade
  7. Justifique a notação de congruência módulo subgrupo H: demonstre que a congruência que já conhecemos (desde FMC1) nos inteiros acaba sendo um caso especial dessa nova: escolhe G, H tais que a≡b (mod m) ⇔ a≡b (mod H)
  8. §§177–178,180
  9. §179
  10. Da §182 apenas resolva os exercícios: x18.101; x18.102
  11. Teorema: HK=KH ⇔ HK≤G
  12. Problemas: Π18.10

26/04/2019

  1. §§181–184
  2. Revise toda a teoria dos grupos que temos até agora
  3. Estude o resto do capítulo de grupos; use as aulas do 2018.2 como guia/ajuda
  4. Problemas: Π18.13; Π18.19; Π18.23

30/04/2019

  1. §§180–185
  2. Revise toda a teoria dos grupos que temos até agora
  3. Estude o resto do capítulo de grupos; use as aulas do 2018.2 como guia/ajuda
  4. Problemas do primeiro intervalo: todos
  5. Problemas do segundo intervalo: Π18.15; Π18.18 todos exceto o Π18.18

06/05/2019

  1. §§184–185
  2. §§186–187
  3. Problemas: Π18.21; Π18.22; Π18.23; Π18.24; Π18.25

08/05/2019

  1. Capítulo 18: §188
  2. Capítulo 18: §189
  3. Capítulo 19: todo (§§190–195)
  4. Problemas: Π18.26; Π19.1

10/05/2019

  1. Estude os gabaritos (ámbos!)
  2. Capítulo 19: todo (§§190–195)
  3. Problemas: Π19.1

13/05/2019

  1. Capítulo 20: §§197–199
  2. Capítulo 20: todo

18/05/2019

  1. Existem irracionais a,b tais que ab é racional?
  2. Dado que π,e são transcendentais; algum dos π + e, eπ é racional?
  3. O contexto histórico do capítulo 21

20/05/2019

  1. Capítulo 21: §§205–213

22/05/2019

  1. Resolva finalmente o homework do dia 20/05/2019
  2. Capítulo 21: §§214–218

24/05/2019

  1. Resolva o problema de casamentos infinitos e escreva uma demonstração do teorema CSB
  2. Entenda a demonstração (amoroso) do teorema de Cantor e escreva uma demonstração formal
  3. Programe os programas do «Intervalo para hackear»
  4. Capítulo 21: todo até a §219 (com o x21.29).
  5. Problemas: Π21.1; Π21.2; Π21.3; Π21.4; Π21.7
  6. Programe o Code-it c21.6.
  7. Problemas: Π18.12; Π21.6

27/05/2019

  1. Capítulo 21: §§219–224
  2. Resolva o problema dos casamentos infinitos e demonstre o teorema de Bernstein (CSB)
  3. Estude bem o problema do «Áristos vs Blammenos» e tente resolvê-lo sozinho antes de olhar na resposta depois do «spoiler alert»
  4. Problema: Π21.5.

29/05/2019

  1. Capítulo 22: §§225–231232 (adicionei a §227)

31/05/2019

  1. Capítulo 22: §§233–239
  2. Problemas: todos do primeiro intervalo de problemas

03/06/2019

  1. Capítulo 22: §§240–243

06/06/2019

  1. Capítulo 22: §§241–244
  2. Justifique as definições de adição e de multiplicação: a recursão usada não é imediata pelo teorema da recursão mas pode ser reduzida pra ser; como?

07/06/2019

  1. Capítulo 22: §§245–247
  2. Demonstre o Teorema Schröder–Bernstein formalmente (sem falar de casamentos)
  3. Demonstre o princípio da boa ordem para o sistema Peano que construimos
  4. Problemas: Π22.9; Π22.10; Π22.11; Π22.12; Π22.13; Π22.14

10/06/2019

  1. [fmcbook]: Capítulo 23: §§251–252 (vou ficar adicionando material nesse capítulo assim que for possível, então fiquem verificando/baixando frequentemente).
  2. [DP]: Itens 1.1–1.33
  3. [DP]: Exercícios (pp. 25–32): 1.1; 1.2; 1.3; 1.4; 1.5; 1.9; 1.12; 1.13; 1.14; 1.16; 1.17

12/06/2019

  1. Justifique formalmente o termo «preordem»
  2. [DP]: Itens 1.34–1.38
  3. [DP]: Itens 2.1–2.7
  4. [DP]: Exercícios (pp. 25–32): 1.7; 1.8; 1.10; 1.11; 1.23; 1.24; 1.27

18/06/2019

  1. Como definirias o subláttice?
  2. Como definirias o homomorfismo entre láttices?
  3. Como definirias o subláttice gerado por um subconjunto dum lattice L?

19/06/2019

  1. Demonstre (sozinho com notas/textos fechados) o teorema de Knaster–Tarski
  2. Enuncie o princípio da indução Noetheriana
  3. Resolva todo o homework que tu não resolveu na hora certa
  4. Resolva os problemas do capítulo 2 de [DP]
    Cuidado: a definição no [DP] de sublattice não aceita o vazio; por isso ele denota por Sub(L) a colecção dos seus (deles) sublattices de L, e por Sub0(L) a colecção dos nossos sublattices de L. Ou seja:
    Sub0(L) = Sub(L) ∪ {Ø}.

Pontos extra

Unidade 1

Pontos de participação

N T
Tyrone 32Victor Hugo 25
Jessiely 18Misael 4
Douglas 16João Mendes 21
Paulo H. 2 Gabriel Alves 5
Andrécio 3 Danilo 16
Maurício 21Francisco Assis B1
Jonathan 4 Lucas Emanoell 8
Hagliberto 5 José Eduardo 3
Francisco Assis CJ 5 Matheus Z. 3
Matheus Menezes 1 Daniel Oliveira 14
Karine 15Daniel Smith 1
Leo 9 Antonio Thiago 1
Moisés 11
Weverson 1
Mateus Melo 8
Levir 1
Keler 3
Cinthia 1
Adailton 5
Kaio 1

Unidade 2

Pontos de participação

N T
Tyrone 9 João Mendes 12
Jessiely 5 Victor Hugo 9
Franscisco Assis CJ5 Jeckson 8
Moisés 11Gabriel Alves 1
Kaio 7 Danilo 7
Maurício 13Gabriel Henrique 1
Hagliberto 3 Isaac 3
Karine 6 Daniel Smith 2
Jonathan 3 José Bezerra 1
Emanuel Borges 1 Daniel Oliveira 5
Douglas 10
Mateus Melo 4
Weverson 6
Leo 6

Unidade 3

Pontos de participação

N
Tyrone 28
Jessiely 11
Moisés 27
Maurício 39
Douglas 29
Weverson 15
Leo 23
Mateus Melo 8
Jonathan 13
Franscisco Assis CJ13
Allan 9
Karine 11
Keler 2
Kaio 4
Cinthia 15
Rita 3

Histórico de aulas

13/02/2019: Introdução [video]

  • Apresentação dos assuntos principais
  • Erros comuns:
    • Type error
    • Erro de lógica
    • Erro de matemática
    • Erro de semântica
  • Os típos principais: afirmações (tbm: proposições); objetos (tbm: individuais)
  • Diferença entre as duas frases:
    • «Se __A__, (então) __B__.»
    • «Como __A__, (logo) __B__.»
  • Os dois erros principais em definições:
    • Não aceitar objetos que deveriam ser aceitos
    • Aceitar objetos que não deveriam ser aceitos
  • ⇒: ``somente se''; ⇐: ``se''
  • O significado da palavra «equivalente» em matemática
  • Noções primitivas – Definições
  • O contexto duma definição
  • Exemplos de definições na geometria euclideana.
  • Axiomas – Teoremas
  • Sinônimos de «teorema» e seus usos: lema, corolário
  • Hipótese; tese
  • Programando programas vs. provando teoremas
  • Lemmata como funções e bibliotecas de programação
  • Sintaxe vs. semântica
  • Uma linguagem para expressões aritméticas
  • Árvores de derivação
  • Parsing: de forma linear para arvore sintática

15/02/2019: Linguagens [video]

  • Números vs. numerais vs. dígitos
  • A notação BNF
  • Uma gramática em BNF para a linguagem de expressões aritmêticas
  • meta-: linguagens e metalinguagens; variáveis e metavariáveis
  • BNF para a linguagem de lógica proposicional
  • Limitações da linguagem da lógica proposicional
  • A linguagem de FOL

16/02/2019: Provinha 0

18/02/2019: Erros; Linguagens; Demonstrações [video]

  • «A ⇒ B ⇒ ... ⇒ true». E daí?!?
  • Prova errada: por afirmação do conseqüente
  • A vírgula mágica de roubo e seus amigos: «sendo», «com», etc.
  • Como e quando usar o «onde»
  • Diferença entre declarada e definida
  • Caligrafia em notação
  • [Jessiely] a expressão x₁,...,xₙ
  • Açúcar sintáctico e abreviações
  • Convenção: notação infixa
  • Demonstrações: como atacar e como usar cada proposição

20/02/2019: Demonstrações [video]

  • Como atacar e como usar o resto dos conectivos
  • Dar nome ou não?
  • A ordem de quantificadores importa?
  • Como demonstrar que duas formulas da FOL não são logicamente equivalentes.
  • Prova por casos
  • Outsourcing o tratamento de negações: botando pra dentro
  • Negação de fórmula atómica
  • Verdade por vacuidade

22/02/2019: Demonstrações; Naturais, recursão, indução [video]

  • Demonstrações
    • Igualdade
    • Reductio ad absurdum
  • Naturais, recursão, indução
    • Os naturais formalmente (Nat)
    • 3 jeitos de descrever a idéia da definição de Nat
    • «Nada mais.»
    • regras de inferência
    • arvore sintáctica dos numerais de Nat
    • Por que esses nats? O bom e o ruim.
    • Recursão
    • Definindo funções no Nat recursivamente
    • Definindo a adição
    • Calculando usando a definição
    • Focos, casamentos, e substituições
    • Cálculo: 3 + 2 = 5
    • Desafio: definir a multiplicação
    • Recursão «no tal argumento»
    • Casos para cada argumento?
    • Cadê a recursão?
    • O poder da recursão
    • Definição recursiva da multiplicação
    • Cálculo: 3 · 2 = 6
    • Provando propriedades sobre nossas operações
    • A + é associativa
      • O que significa?
      • Posso escrever a afirmação como uma fórmula?
      • Agora, bora provar!
      • Um aparente deadend
      • Não: posso separar casos
      • Prove então!
    • Tentando provar sem indução: separando em casos, e casos, e casos…
    • A idéia da indução

25/02/2019: Nats; recursão; indução [video]

  • Nats: definição e operações
  • Associatividade de adição: tentativa tradicional
  • Como escolher a variável para separar casos
  • O princípio da Indução nos Nats
  • Associatividade da +: primeira demonstração
  • Associatividade da +: segunda demonstração
  • Como escolher a variável para fazer indução
  • «indução "no k"»
  • Comutatividade da +
  • Igualdade sintáctica vs. denotacional
  • Uso de Lemmata
  • Recursão para definir relações
  • Por que aceitar o princípio da indução?
  • O que que têm especial os nats?
  • E sobre os não-nats?
  • Definições inductivas
  • Recursão e indução: dois lados da mesma moeda
  • Cadê princípio de recursão então??

27/02/2019: Nats, recursão, indução; Conjuntos [video]

  • Nats, recursão, indução
    • Outros princípios de indução
    • Indução a partir dum natural n
    • Indução forte
    • Princípio de Boa Ordem
    • Equivalência dos princípios
    • Mais que uma base
  • Conjuntos
    • os «def» em cima de = e de ⟺
    • Tipos de objetos e como introduzí-los
    • Conceito de conjunto
    • Noções primitivas: ser conjunto, pertencer (∈)
    • Conjuntos como “black boxes
    • Igualdade entre conjuntos: A=B
    • Intensão vs extensão
    • Notação
    • Set comprehension (Set-builder notation)
    • Não use «|» como abreviação de «tal que» nem em texto nem nas fórmulas existenciais!
    • Açucar sintáctico no set-builder
    • Erro comum: quantos elementos {x,y,z} tem?
    • As relações binárias: =, ⊆, ⊇, ⊊, ⊋
    • ⊈ vs. ⊊
    • Cardinalidade |A|

01/03/2019: Conjuntos [video]

  • Cuidado: O uso de ⊂ na literatura
  • Definindo o conjunto vazio: nossos deveres
  • O predicado Empty(–)
  • Variáveis livres e ligadas; sombreamento de variável
  • Obrigação de definir notação (nome) para objeto: artigo definido vs. indefinido
  • Provas de existência & unicidade
  • Teorema: existência do conjunto vazio
  • Teorema: unicidade do conjunto vazio
  • O conjunto vazio (Ø)
  • Singletons
  • O conjunto universal
  • Oito proposições sobre o Ø e um conjunto A
  • Escolhendo a ordem de atacar teoremas
  • {Ø} ≠ Ø
  • Operações entre conjuntos e dois jeitos de defini-las
  • As operações binárias: ∩, ∪, \, Δ
  • A operação unária de complemento: ~
  • O operador Powerset (℘)
  • Iterando o ℘ no Ø
  • Cardinalidade de ℘A

08/03/2019: Conjuntos [video]

  • Generalizando as operações de união e intersecção: as operações unárias ⋂, ⋃
  • Intuição sobre os ⋂, ⋃, e ℘ e as {, }
  • Iterando os ⋂, ⋃, e ℘ no Ø
  • tuplas como noções primitivas: igualdade, tamanho
  • tuplas como black boxes
  • projeções: πi
  • Implementando um tipo: 3-tuplas

11/03/2019: Conjuntos [video]

  • Recap
  • O tipo de 1-tuplas
  • O tipo de 0-tuplas
  • A única 0-tupla: ()
  • Como pensar no tipo void da C
  • Equações fundamentais de tuplas
  • Produto cartesiano (×)
  • Cardinalidade do A×B
  • Definindo o Aⁿ
  • Implementação-agnóstico
  • Seqüências
  • outras notações
  • União e Intersecção de seqüências de conjuntos
  • Famílias indexadas
  • Exemplo: Os conjuntos Aₚ e Cₚ de todos os ancestrais e todos os filhos de p
  • Traduzindo afirmações da linguagem natural para relações entre conjuntos e vice-versa
  • União e Intersecção de famílias indexadas de conjuntos
  • Família indexada como generalização de n-tuplas e seqüências
  • Σ vs. ⋃
  • Riemann's rearrangement theorem
  • Produto cartesiano generalizado (de família indexada de conjuntos)
  • Um exercício para aprender como atacar e como usar alvos que involvem operações grandes

13/03/2019: Conjuntos; Funções [video]

  • Conjuntos
    • Conjuntos disjuntos dois-a-dois («pairwise disjoint»): definição com e sem índices
    • Os operadores binários ∪ e ∩ como açucar sintático (definido pelos operadores unários ⋃ e ⋂ respeitivamente)
    • Como usar um fato do tipo D≠Ø em nossas provas: «Seja dD
    • lim inf, lim sup
  • Funções
    • Conceito, notação, igualdade.
    • Igualdade extensional vs. intensional
    • Duas religiões sobre funções e seus black boxes
    • O conjunto (A→B) (também denotado por BA)
    • (Co)domínios vazios.
    • Diagramas internos e externos.
    • Como definir e como não definir funções
    • Expressões com buracos.

15/03/2019: Conjuntos; Funções; Prova 1.1 [video]

  • Conjuntos
    • Seqüências de conjuntos: lim inf, lim sup, lim
    • Cuidado: “sejando” membros de conjuntos sem usar apenas uma variável
  • Funções
    • Diagramas internos e externos
    • Como definir e como não definir funções
    • Diferença entre f(x) e f
    • Expressões com buracos
    • A notação lambda

18/03/2019: Funções [video]

  • Mini-sermão sobre provas escritas
  • Um toque de λ-cálculo
  • Computação com λ
  • β-redex; β-reducção
  • α-renomeamento (α-equivalência) e captura de variável
  • η-equivalência
  • essas idéias vistas em conjuntos (set builder)
  • first-class citizens
  • desafio: achar almas (lambdas) para habitar corpos (típos)
  • funções de graça: identidade
  • composição
  • mais funções de graça: inclusão A↪B
  • leis de composição
  • operações totais vs parciais
  • associatividade da composição
  • comutatividade?
  • possui identidade(s)?
  • aplicação parcial
  • mais funções de graça: restricção
  • diagramas comutativos

20/03/2019: Funções [video]

  • constante: três definições
  • função com (co)domínio vazio
  • função característica
  • Unix shell: um calculador de booleanos
  • if-then-else expressions vs branching statements
  • mais funções de graça:
    • cross (f×g);
    • pair (f,g);
    • pointwise (f*g)
    • diagonal Δ
  • Funções injetoras, sobrejetoras, bijetoras: formalmente e informalmente
  • Exemplo: codificação dos pares de Nats nos Nats
  • Cardinalidade de (A↣B)

22/03/2019: Funções [video]

  • iterações
  • uma prova errada não quis dizer teorema errado
  • conseqüência de teorema errado não quis dizer que a conclusão é errada
  • a composição preserve as “-jetividades”
  • a frase «pela escolha de»
  • inversas com pontos–“por dentro”
  • exercícios
  • leis da inversa
  • o que podemos concluir se uma composição é bijetora

25/03/2019: Funções [video]

  • uma viagem épica: mono e epi
  • estilo pointfree (ou pointless)
  • imagem e preimagem
  • problema na notação
  • possível definição alternativa de preimagem
  • problema na notação alternativa f(X)?
  • funções de ordem superior
  • a função-imagem respeita as uniões e as intersecções?

27/03/2019: Funções [video]

  • função-imagem: nível coração
  • funções parciais
  • funções não-determinísticas
  • funções para implementar outros típos
  • seqüências, famílias indexadas
  • restrição com buraco: seu tipo
  • tipos dependentes
  • currificação
  • programando funções: escopos; dados; alvos;
  • definindo funções por recursão
  • quantas das k,d,c aceitas como definidas?

29/03/2019: Funções; Prova 1.2 [video]

  • definindo funções por recursão
  • associatividade algebrica de operador vs. associatividade sintáctica de conectivo
  • higher-order fun
  • um λ não terminante
  • Quantas idempotentes no 3?
  • de união para o coproduto

01/04/2019: Aula cancelada

03/04/2019: Funções; Categorias; Relações [video]

  • funções
    • Sermão: poluição do escopo
    • de união para o coproduto
    • o problema de definir a f∪g
    • união disjunta ; coproduto ; sum type
    • conjuntos isomórficos/isómorfos
    • definindo a f+g
    • produtos vs. coprodutos: nível coração
  • categorias
    • definição
    • exemplos
    • o conceito de produto
  • relações
    • conceito, notação
    • diagramas internos
    • definindo relações
    • igualdade
    • intensional vs extensional
    • construções e operações em relações
    • relação oposta
    • composição
    • RT=T? RF=F?

05/04/2019: Relações [video]

  • notação: R∘S vs S∘R
  • propriedades de relações
  • fechos informalmente
  • a ordem dos fechos importa?
  • fechos formalmente
  • potências/iterações de relação
  • preguiças nos diagramas internos
  • um exemplo de fecho
  • relações de equivalência
  • classes de equivalência

08/04/2019: Relações; Programação [video]

  • Relações
    • fechos: top-down vs bottom-up
    • partições
    • o conjunto quociente
    • enxergando o conjunto quociente
    • subconjuntos finitos vs cofinitos
    • relações de ordem
    • relações recursivas
    • relações de ordem superior
    • perigos de funções mal-definidas
    • ε-perto é uma relação de equivalência?
  • Programação
    • paradigmas
    • programação imperativa (procedural; OO)
    • puramente OO
    • programação declarativa (funcional; lógica)
    • side effects
    • lazy vs strict
    • static vs dynamic types
    • puramente funcional

10/04/2019: Relações; Programação [video]

  • Relações
    • Quantas relações de equivalência num conjunto com 3 membros?
  • Programação
    • Lazy vs strict (call-by-name, call-by-value, call-by-need, call-by-push-value)
    • turing-completeness
    • higher-order
    • dependent types
    • Lisps
    • Abuso de linguagens
    • Conselhos
    • Programação Funcional
    • Indução e recursão nas listas
    • Programação Lógica
    • Funções como relações
    • Entendi!

12/04/2019: Programação; Algebra abstrata; Teoria dos grupos; Prova 1.3 [video]

  • Programação
    • Turing complete vs Pacman complete
    • Bancos de dados
  • Algebra abstrata
    • História: de Euclides até Galois
    • uns problemas antigos e abertos na época
    • construções com régua e compasso
    • raízes de polinómios com fórmulas
    • a idéia da álgebra abstrata
    • Conjuntos estruturados
    • abusos notacionais
  • Teoria dos grupos
    • permutações
    • notação com parenteses e com cíclos
    • achando os membros do S₃
    • leis abstratas satisfeitas por S₃
    • primeira defição de grupo
    • ℘A é grupo com qual das operações binárias conhecidas de conjuntos?

15/04/2019: Teoria dos grupos [video]

  • Umas definições de grupo, com outros tipos de estrutura
  • Grupos abelianos
  • O que significa teoria dos grupos
  • Teorema: unicidade de identidade
  • Escolhendo leis
  • Nãœxemplo de grupo: strings com concatenação
  • Teorema: leis de cancelamento: (GCL) & (GCR)
  • operando por o mesmo lado
  • propriedade de igualdade: substituir iguais por iguais
  • cuidado com o uso do "⇒" nas demonstrações
  • Teorema: unicidade dos inversos
  • não podemos operar nos dois lados por lados diferentes
  • Notação: Grupos aditivos e multiplicativos
  • potências em grupos
  • Propriedades de inversos
  • G abeliano ⇒ (ab)⁻¹ = a⁻¹b⁻¹
  • Enxergando a mesma igualdade em maneiras diferentes
  • Teorema: inverso da identidade
  • Como podemos provar que algo é inverso/identidade?
  • Umas respostas erradas
  • Teorema: resolução de equações: (RESL) & (RESR)
  • Critério: Identidade e inversos mais baratos: (Id-bar) & (Inv-bar)
  • Teoremas: inverso de inverso & inverso de produto
  • {2ⁿ | n inteiro} vira um grupo com adição? Com multiplicação?

17/04/2019: Teoria dos grupos [video]

  • exemplos e nãœxemplos de grupos
    • números com adição
    • definição recursiva do 𝐧 = {0,…,n-1}
    • adição módulo n
    • matrízes com adição
    • números com multiplicação
    • multiplicação módulo n
    • os inversos chegam em pares/casais
    • matrízes com multiplicação
    • (℘A;Δ)
    • strings com concatenação
    • funções reais com pointwise adição e multiplicação
    • as potências de 2
  • duas maneiras de tomar membros dum conjunto indexado
  • previously on FMC2…
  • escolhendo leis (axiomas)
    • como demonstrar que algo não é demonstrável pelumas leis
    • Critérion: G finito + (G0) + (G1) + (GCL) + (GCR) ⇒ G grupo
    • Critérion: (G0) + (G1) + (G2L) + (G3L) ⇒ G grupo
    • o que é «critérion»
    • econômia vs claricidade/intuitividade
    • Critérion: (G0) + (G1) + (G2R) + (G3R) ⇒ G grupo
    • modularidade
    • (G0),(G1),(G2L)
    • magma, semigrupo, monóide, grupo, grupo abeliano
  • ordem de grupo: o(G) ou |G|
  • tem grupos de ordem 0?
  • tem grupos de ordem 1?
  • tabelas Cayley
  • jogando grupoku
  • o grupo ({0,1,2};+₃) e sua tabela Cayley
  • potências de membros de grupo
  • as potências aⁿ para n=-1,0,1,2,…
  • duas definições razoáveis para o a⁻²
  • Teorema: (a⁻¹)² = (a²)⁻¹
  • Definição: As potências aⁿ para n inteiro
  • um diagrama cuja comutatividade é a lei (a⁻¹)² = (a²)⁻¹
  • um diagrama cuja comutatividade é a lei (ab)⁻¹ = b⁻¹a⁻¹
  • ∀a∀b (ab)⁻¹ = a⁻¹b⁻¹ ⇐?⇒ G abeliano

22/04/2019: Teoria dos grupos [video]

  • Definição: ordem de membro de grupo: o(a)
  • membros com ordem infinita e finita em grupos
  • quantas ordens diferentes dentro dos membros do S₃
  • pelo menos n potências
  • «sem perda de generalidade»
  • no máximo n potências
  • tomando membros arbitrários de conjuntos indexádos
  • sermão: divisão de Euclides
  • o(a) = ∞ ⇒ todas as potências de a são distintas
  • aᵐ = e ⇔ o(a)|m
  • Subgrupos: intuição, conceito, definição
  • Exemplos e nãœxemplos
  • Observação: associatividade de graça no H
  • Observação: H e G não podem ter identidades diferentes
  • Critério: quando H é não vazio, basta fechado pela operação e pelos inversos
  • Critério: quando H é finito e não vazio, basta fechado pela operação

24/04/2019: Teoria dos grupos [video]

  • one-test critérion
  • a R(H) é uma relação de equivalência
  • ≤ é uma ordem parcial
  • intersecção de subgrupos é subgrupo
  • união de subgrupos é subgrupo?
  • Geradores
  • subgrupo gerado por membro de grupo
  • subgrupo gerado por dois membros de grupo
  • subgrupo gerado por subconjunto de grupo
  • palavras
  • bottom-up
  • top-down
  • conjuntos convexos, bichos e subbichos
  • não intersectarás famílias vazias
  • exemplos de geradores, e grupos cíclicos
  • três casos para decidir se a relaciona com b
  • coclasse direitas e esquerdas
  • as coclasses direitas é uma partição do G
  • coclasses direitas e a relação anterior
  • congruência módulo subgrupo
  • por que as coclasses direitas?
  • módulo direito e módulo esquerdo
  • as coclasses têm a mesma cardinalidade?
  • atores
  • HK≤S₃? KH≤S₃?

26/04/2019: Teoria dos grupos [video]

  • assim que tiver um H≤G…
  • H = {e,φ}; K = {e,ψφ}
  • 𝓛(K) =?= 𝓡(K)
  • conjuntos indexados
  • igualdade e tomando membros arbitrários
  • o teorema de Lagrange
  • índice de subgrupo em grupo
  • o que precisamos mais demonstrar?
  • exemplos com grupos de números
  • corolário: de novo: HK≤S₃? KH≤S₃?
  • corolário: subgrupos de grupo com ordem primo
  • corolário: o(a) | o(G)
  • corolário: a^(o(G)) = e
  • teoria dos números revisitada: o teorema de Euler
  • HK = KH ⇔ HK ≤ G
  • subgrupos normais: L(H) = R(H)
  • assim que tiver um N⊴G…
  • afastando até G/N
  • C*D = ?
  • o grupo quociente: G/N
  • conjugação em grupos
  • «é conjugado de» é uma relação de equivalência
  • N⊴G ⇔ …
  • {e,ψ,ψ²}⊴S₃?

06/05/2019: Teoria dos grupos [video]

  • subgrupos normais e o grupo quociente
  • justificar o nome/notação: congruência (mod H)
  • congruências
  • simetrias
  • as simetrias do triângulo
  • o grupo Dih₃
  • Dih₃ ≅ S₃
  • grupos isómorfos
  • propriedades grupoteóricas os subgrupos de Dih₃ e diagramas Hasse
  • (homo)morfismos de grupos
  • preservar/respeitar estrutura
  • primeiro momento que a assinatura da estrutura de grupo importa?
  • critérion de homomorfismo
  • (mono,epi,split-mono,split-epi)-morfismos
  • isomorfismo; isómorfos/isomórficos
  • «preservar estrutura» com diagramas comutativos
  • diagramas de Hasse
  • (℘{1,2,3} ; ⊆)
  • (ℕ ; ≤)
  • (ℕ ; |)
  • (Sub(Dih₃) ; ≤)
  • homework: Sub(Dih₄)
  • Dih₄ vs. S₄
  • o(Dih₄)

08/05/2019: Categorias; Teoria dos grupos; Álgebra abstrata [video]

  • Categorias
  • definição e revisão
  • três categorias: SET, N(≤) e N(|)
  • lembrete de produtos e coprodutos
  • objetos iniciais e terminais numa categoria
  • categoria dos grupos GRP
  • iniciais e terminais nessas quatro categorias
  • «ao menos de isomorfismo»
  • mono, epi, split mono, split epi, iso
  • Teoria dos grupos
  • kerφ (definição)
  • kerφ ≤ Α
  • kerφ ⊴ Α
  • Teorema: kerφ singleton ⇔ φ injetiva
  • * injecção vs mono
  • o primeiro teorema de isomorfismo
  • kernel ⇔ normal
  • Outras estruturas algébricas
  • Monóides
  • definição
  • submonóides e homomorfismos
  • critéria?

10/05/2019: Álgebra abstrata; Prova 2 [video]

  • Hom(G,H) em categorias
  • Hom(G,H) é um grupo? abeliano?
  • grupos: mais -morfismos: endo-; auto-
  • outras estruturas
  • anel
  • mais exemplos de aneis: inteiros módulo m, End(G)
  • primeiras conseqüências das leis de anel
  • zerodivisores
  • domínios de integridade e domínios de cancelamento
  • DI ⇐?⇒ DC

13/05/2019: Álgebra abstrata; Os números reais [video]

  • revisão: estruturas algébricas
  • teorema: domínio de integridade ⇔ domínio de cancelamento
  • corpos
  • teorema: domínio de integridade finito ⇒ corpo
  • reticulado
  • anel booleano
  • exemplos de reticulados
  • reticulado bounded (limitado)
  • corpos
  • corpos ordenados
  • como diferenciar os reais dos racionais?
  • ordem densa
  • bounded
  • bounded above/below; upper/lower bound
  • desenhando os dois corpos ordenados
  • o corpo ordenado dos racionais tem buracos
  • lei de completude
  • supremum/infimum
  • sup/inj; lub/glb; join/meet; ⋁/⋀
  • corpo ordenado completo
  • unicidade dos reais
  • único «a menos de isomorfismo»
  • entendi tudo!(?)

15/05/2019: paralisação/protesto

  • sendo um idiota (in?)útil participei no nosso protesto
  • a fórmula da água tenho quase certeza que é ou
    (b±√(b²-4ac)) / 2a
    ou
    e-iπ + 1 = 0
    (depende da fonte da água)

17/05/2019: Os reais; História [video]

  • recap: corpos ordenados completos; infimum, supremum
  • infA ≤ supA ?
  • infimum e supremum do Ø
  • calculus de verade
  • definição de limite
  • ε-perto
  • o que preciso demonstrar para usa a frase «x,y são...»
  • definição como jogo
  • mais gírias matemáticas
  • «a partir de...»
  • «eventualmente...»
  • não ter limite
  • definição de continuidade
  • interpretação geométrica da expansão decimal de reais
  • algébricos e transcendentais
  • exemplos e nãœxemplos
  • o √2 é algebrico
  • duas definições equivalentes de algébrico
  • história: de 1700 até Cantor
  • números transcendentais
  • Cantor sobre series Fourier (1870,1871,1872)
  • convergência ponto a ponto (pointwise)
  • pontos de acumulação
  • conjunto derivado
  • nascimento da teoria dos conjuntos: os conjuntos como objetos de estudos (first-class citizens)

20/05/2019: O paraíso de Cantor [video]

  • Hermite e von Lindemann
  • existem a e b irracionais tais que aᵇ racional?
  • alguem dos π + e, πe é irracional?
  • como comparar conjuntos infinitos
  • as relações =c, ≤c, <c
  • 2ℕ =c ℕ
  • definições: contável, finito
  • cardinalidade
  • cardinais vs ordinais
  • jogos imortais de enumeração [Smullyan]
  • qualquer conjunto finito é contável
  • o conjunto de naturais é contável
  • o que estamos fazendo formalmente?
  • definição: enumeração de conjunto
  • os inteiros são contáveis
  • os racionais são contáveis
  • ℕ² e o primeiro argumento diagonal de Cantor
  • stratificação
  • Kleene star
  • os strings finitos dum alfabeto finito são contáveis
  • strings com alfabeto infinito: ℕ*
  • ℘fℕ; ℘f℘fℕ; ℘fᵏℕ
  • conjuntos incontáveis
  • o segundo argumento diagonal de Cantor
  • união contável de contáveis é contável
  • numeros selvagens (ou domesticados?)
  • racionais vs. irracionais
  • algebricos vs. transcendentais
  • teorema fundamental da algebra
  • primeira grande aplicação da teoria de Cantor
  • =c é uma relação de equivalência?

22/05/2019: O paraíso de Cantor [video]

  • ≤c é uma preordem
  • ≤c não é antissimétrica
  • ≤c é ``equiantissimétrica''
  • todos os intervalos ``da mesma forma'' são equinúmeros
  • respeitando e desrespeitando equinumerosidades
  • A x B =c A' x B'
  • ℘A =c ℘A'
  • (A → B) =c (A' → B')
  • uniões e intersecções
  • currificação de novo
  • A ≤c B: afirmações equivalentes
  • A ≤c B ⇐?⇒ existe sobrejetora f : B → A
  • A ≤c B ⇒?⇒ existe sobrejetora f : B → A
  • A ≤c B ⇐?⇐ existe sobrejetora f : B → A
  • TEASER/SPOILER: axioma da escolha
  • por que o 2o argumento diagnoal de Cantor não serve para os racionais?
  • Cantor vs Liouville
  • procurando bijecções
  • teorema de Bernstein (CSB)
  • ℝ, ℝ², ℝ³, ℝⁿ, (ℕ→ℝ): equinúmeros?
  • casamentos infinitos [Smullyan]

24/05/2019: O paraíso de Cantor [video]

  • bijecções entre intervalos de reais
  • casamentos infinitos: uma dica
  • o conjunto de Cantor
  • teorema de intervalos aninhados de Cantor
  • Devil's staircase
  • dicas para demonstrar equinumerosidades
  • codificações
  • trocando conjuntos por equinumeros
  • teorema de Cantor (com depressivos)
  • Uma carta de Cantor para Dedekind

27/05/2019: O paraíso de Cantor; O paradoxo de Russell [video]

  • lembrete: dica do problema dos casamentos
  • conseqüências do teorema de Cantor
  • aleph-0, beth-0, e continuum: ℵ₀, ℶ₀, 𝔠
  • Continuum Hypothesis (CH)
  • comparabilidade de cardinalidades
  • hypergame de Zwicker
  • o hypergame é terminante?
  • quantos programas de tipo Nat → Nat tem?
  • Áristos vs Blammenos
  • da Devil's staircase para medida
  • um toque de teoria de medida
  • o paradoxo de Russell

29/05/2019: Teoria axiomática dos conjuntos ZF [video]

  • recap: o paradoxo de Russell
  • metáforas para descrever o paradoxo
  • resoluções
  • teoria dos tipos (Russell)
  • teoria dos conjuntos (Zermelo)
  • leis vs axiomas
  • noções primitivas: pertencer e ser conjunto
  • o princípio da puridade
  • fundação de matemática
  • revisão: FOL
  • traduzindo de e para a FOL dos conjuntos
  • interpretação de uma FOL
  • tautologias
  • a palavra de Zermelo
  • ZF1 [Extensionalidade] e suas conseqüências
  • ZF2 [Emptyset] e suas conseqüências
  • existência e unicidade do vazio
  • Ø
  • ZF3 [Pairset] e suas conseqüências
  • mais conjuntos
  • {–,–}; {–}
  • com ZF1–ZF3 podemos construir apenas conjuntos com cardinalidade 0, 1, ou 2
  • uma infinidade de conjuntos
  • um padrão nas formulas de ZF
  • ZF4 [Separation] e suas conseqüências
  • sua interpração
  • {x∈–|–}
  • uma comparação com o Princípio da Comprehensão Geral
  • o paradoxo de Russell revisitado
  • como usar o [Separation]
  • o universo não é um conjunto
  • ZF5 [Poweset] e suas conseqüências
  • ℘–
  • conjuntos de qualquer cardinalidade finita
  • –∩–; ⋂–
  • ZF6 [Unionset] e suas conseqüências
  • ⋃–; –∪–
  • classes vs conjuntos; classe própria

31/05/2019: Teoria axiomática dos conjuntos ZF [video]

  • ZF1–ZF6: recap
  • –\–
  • –∪–
  • –Δ–
  • teorema dos singletons
  • implementando outros tipos
  • Russell: de paradoxo para teorema
  • o par ordenado (2-tupla)
  • o par de Kuratowski
  • relações; funções; famílias
  • espaços de relações e funções
  • conseguimos implementar o powerset-finito?
  • ZF1–ZF6: impossibilidade de construir o conjunto dos naturais
  • números cardinais e sua aritmética
  • união disjunta (coprodúto)
  • dois enunciados do ZF7: Zermelo; von Neumann
  • a existência de quantos conjuntos infinitos é garantida pelos axiomas ZF1–ZF7?

03/06/2019: Teoria axiomática dos conjuntos ZF [video]

  • recap: os ZF1–ZF6
  • união-disjunta na ZF
  • mais sobre a aritmética dos cardinais e suas leis
  • grupos e conjuntos estruturados na ZF
  • o sucessor de Zermelo e de von Neumann
  • o ZF7 e suas conseqüências
  • temos de graça uma implementação do conjunto dos naturais
  • axiomas de Peano
  • existência dos naturais: top-down
  • unicidade dos naturais
  • Teorema da Recursão
  • aproximações de função: bottom-up
  • funções parciais
  • funções compatíveis e incompatíveis

05/06/2019: Teoria axiomática dos conjuntos ZF [video]

  • recap: construção dos naturais
  • existência dos naturais
  • unicidade dos naturais
  • teorema da recursão
  • funções parciais
  • funções compatíveis e incompatíveis
  • função converge
  • igualdade de Kleene
  • aproximações de funções
  • lemma: as aproximações são compativeis
  • como usar o princípio da indução
  • definindo operações e relações nos naturais
  • isomorfismos respeitam tudo isso
  • esboço: como implementar os outros conjuntos de numeros
  • de naturais para inteiros para racionais para reais para complexos
  • uma idéia para implementar os inteiros
  • quantos axiomas encontramos até agora?
  • axioma vs. esquema axiomático

07/06/2019: Teoria axiomática dos conjuntos ZF [video]

  • igualdade de Kleene
  • outras formas de recursão: com parametros, etc.
  • Dedekind-(in)finito na ZF1–ZF6
  • boas ordens e o princípio da boa ordem
  • Construindo os inteiros
  • Construindo os racionais
  • Construindo os reais
  • completude com suprema (ou infima)
  • completude com seqüências
  • seqüência convergente
  • seqüência Cauchy
  • definição do conjunto dos reais (Cantor)
  • Dedekind cuts
  • downwards-closed
  • resto ta definição de Dedekind cut
  • definição do conjunto dos reais (Dedekind)
  • definição das operações e relações entre reais
  • hipótese do continuum e da comparabilidade de cardinalidades
  • Outros axiomas
  • ZF8 [Replacement] e suas conseqüências
  • Class-functions e fórmulas function-like
  • ZF9 [Foundation] e suas conseqüências
  • AC: Axiomas de escolha e suas conseqüências
  • Antifoundation de Aczel
  • conseqüências controversiais do AC
  • versões de escolha mais fracas que a do AC
  • outras teorias de conjuntos
  • limitações
  • outros fundamentos
  • casamentos: discussão
  • Áristos vs Blammenos: discussão
  • limitações de computação
  • o halting problem
  • tem Nats infinitos na linguagem?
  • o problema de Josephus não tem nada a ver com o ZF9
  • a comparabilidade das cardinalidade é demonstrável?
  • ataques injustos contra o axioma da escolha
  • igualdade e o axioma da extensionalidade

10/06/2019: Teoria da ordem [video]

  • recap
  • posets
  • ordem: fraca vs estrita
  • máximo/mínimo
  • upper/lower bounds
  • A ≤ m ; m ≤ A
  • subposet
  • maximal/minimal
  • relação de cobrir
  • diagramas Hasse
  • pontos incomparáveis
  • ↑x ; ↓x
  • ↑A ; ↓A
  • downset ; upset
  • exemplos: posets feitos por números
  • naturais com ordem comum
  • naturais com ordem de divide
  • inteiros com ordem comum
  • exemplo: números (ordinais como posets)
  • poset discreto
  • exemplo: números (como posets discretos) [1:00:42]
  • flat posets
  • bottom ou zero ; top ou one
  • construindo ordens
  • poset discreto
  • lift(P)
  • P⊎Q ; P⊕Q
  • desenhando posets construidos por ⊕ e ⊎
  • associatividade dos ⊎, ⊕
  • exemplo: powerset
  • duas maneiras de desenhar
  • dual(P)
  • lift(P) como somatório
  • 𝒪(P): o poset de todos os downsets de P
  • 𝒪(N) = ?

12/06/2019 [video]

  • chain, antichain
  • exercício: downsets dos N, Z, Q, R.
  • ordinais de von Neumann como posets
  • strings (finitos ou infinitos)
  • espaços de funções parciais como posets
  • P×Q
  • com (anti)lexicográfica
  • com componentwise
  • como desenhar o Hasse dela
  • Pᴬ, ou seja, (A→P) com pointwise
  • por que «preordem»?
  • a categoria POS dos posets
  • order-preserving (monótona); -embedding; -isomorfísmo
  • critérion de embédding (e logo de isomorfismo)
  • definição categórica de iso?
  • sup/inf, lub/glb, join/meet
  • duas maneiras de faltar o join ou o meet
  • ache os joins: a∨b, b∨c

14/06/2019: paralisação/protesto

14/06/2019: ZF; Ordem [video]

  • ZF
    • {–,...,–}
    • construindo uns conjuntos
    • uma classe que é conjunto
    • duas classes próprias
    • Someset is the new Emptyset
    • Triset it is the new Pairset
    • umas conseqüências do foundation
    • Replacement is the Pairset, Separation, etc.
    • a φ que definimos para ser Peano-isomorfismo é sobrejetiva
    • e ela respeita a soma
  • Ordem
    • ordem pointwise e seus joins e meets
    • ordem pointwise e sua relação de cobrir nos (ℕ→ℕ) e (ℝ→ℝ)
    • ordem antilexicográfica e o P·Q
    • como desenhar uns posets
    • são reticulados?
    • dá pra embutar um em outro?

17/06/2019: Teoria da ordem [video]

  • desenhando posets de naturais com divisibilidade
  • reticulado e reticulado completo
  • desafio: construir um poset tal que...
  • tem poset isomorfo com um powerset poset?
  • os naturais com divisibilidade eh um poset
  • join e meet do vazio e do P (P poset)
  • D₀ não é isomorfo com nenhum powerset poset
  • os primeiros ordinais de von Neumann
  • Lembrando: P×Q ; P·Q ; P⊎Q ; P⊕Q
  • mais sobre ordinais
  • a multiplicação não é comutativa
  • o que podemos concluir sobre os ordinais α,β se...?
  • como os ordinais contáveis aparecem
  • números transfinitos: cardinais vs. ordinais
  • aritmética ordinal
  • Lattices: reticulados algebricamente
  • Lattices e reticulados: conexão
  • Chains
  • length
  • no infinite chains ⇒?⇒ length infinito?
  • ACC e DCC

19/06/2019: Teoria da ordem [video]

  • reticulados
  • homomorfismos entre reticulados
  • subreticulado
  • subreticulado gerado por conjunto
  • ACC, DCC, axioma da escolha
  • relações bem-fundadas e indução Noetheriana (bem-fundada)
  • teorema de ponto fixo de Knaster–Tarski
  • previsão das notas

21/06/2019: Assuntos auxiliares; Prova [video]

  • Tô pronto pra prova
  • Resolução da Prova 3.1
    • o princípio da boa ordem e o princípio da indução nos naturais
    • o axioma CONS na ZF
    • embutindo ordinais nos racionais
    • um teorema de ponto fixo de Kleene
  • Ordinais: recursão e indução transfinita
    • Como parecem os primeiros ordinais
    • Recursão e indução transfinita
  • λ-calculus
    • recap: α, β, η, ...
    • implementações no λ-calculus
    • Nats no λ-calculus
    • Church numerals
    • succ
    • Bools no λ-calculus
    • Church booleans
    • not
    • ifthenelse
    • plus, times, etc.
    • fixpoints e definições recursivas
    • desafio: definir o factorial
    • o Y combinator
    • e agora..?

Futuro (fluido)

26–28/06/2019: Prova de reposição

Last update: Sat Jun 22 20:38:24 -03 2019