2020.1 FMC2, turmas de Thanos

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;
  }

15/01/2020

1. Assista minhas aulas relevantes do FMC1/2019.2 (até 16/09/2019)
2. Estude o capítulo «Estratégias de provas».
3. Estude o capítulo «Linguagens».
4. Estude o capítulo «A linguagem de lógica proposicional».
5. Estude brutalmente o capítulo «Os números naturais: recursão; indução».
6. Estude os capítulos 1–3 de Velleman.
7. Brinque com Haskell ou PureScript.
8. Installe o Coq; dê uma lida no «Preface» do SF1 (link na Bibliografia); estude o capítulo «Basics» do SF1.

23/02/2020

1. Podemos ler o « ⇔ » como «se e somente se». Qual das duas partes dele (⇐ e ⇒) corresponde no «se» e qual no «somente se»?
2. Podemos ler o « ⇔ » como «é suficiente e necessário para». Qual das duas partes dele (⇐ e ⇒) corresponde no «é suficiente para» e qual no «é necessário para»?
3. Resolva os A,B da provinha 0.
4. Pense sobre o resto dos conectivos: como faria sentido atacar e como usar?
5. Já fez o homework anterior?

28/02/2020

1. Defina as (∃!x)[φ(x)] e (∃!x∈A)[φ(x)] como açúcares sintácticos do que temos até agora.
2. Defina o predicado Singleton(–)
3. Estude as secções §§113–117.
4. Estude a secção §118.

02/03/2020

1. (∃!x)[φ(x)] ⇐?⇒ (∃z)(∀x)[φ(x)⇔x=z]

04/03/2020

1. Estude a secção §119.
2. Estude a secção §120.
3. Estude a secção §121.
4. Estude a secção §122.
5. Estude a secção §123.

06/03/2020

1. Nesse problema é proibido usar os «feitiços fortes»: nem LEM, nem dupla negação, e logo não podes demonstrar algo por Reductio ad absurdum. E logo, para atacar uma disjunção precisa escolher um dos dois componentes e matá-lo!
   Suponha que P denota uma proposição arbitrária. Quais das propriedades seguintes consegues demonsrar?
   1. P⇒¬¬P
   2. P⇐¬¬P
   3. ¬¬(P∨¬P)
   4. se P⇒Q então ¬Q⇒¬P
   5. se ¬Q⇒¬P então P⇒Q
2. Para aquela das duas últimas que tu não conseguiu demonstrar (por justa causa!), tem como demonstrar «quase» isso, ou seja, tem como demonstrar uma coisa parecida mas mais fraca. Adivinha qual é, e demonstre!

07/03/2020

1. Estude brutalmente o capítulo «Os números naturais: recursão; indução». (Foi hw desde 24/02/2020.)
2. Resolva as questões de recursão/indução de FMC1 dos semestres passados, especialmente do 2019.2.

09/03/2020

1. Resolva os problemas: Π10.1; Π10.2; Π10.3
2. Resolva os problemas: Π10.11; Π10.12

10/03/2020

1. Estude a secção §125: Tuplas
2. Estude a secção §126: Produto cartesiano

11/03/2020

1. Estude a secção: Seqüências
2. Π10.4
3. Π10.5
4. Π10.6
5. Π10.7
6. Π10.8
7. Π10.13
8. Π10.14
9. Π10.15
10. Π10.16
11. Π10.17
12. Π10.18

13/03/2020

1. Defina a União e Intersecção de famílias indexadas de conjuntos. Verifique tua definição (olhando no fmcbook).
2. Estude o resto do capítulo «Conjuntos»!
3. Resolva o resto dos problemas!

16/03/2020

1. Estude a secção §135: Conceito, notação, igualdade
2. Estude a secção §136: Diagramas internos e externos

31/03/2020

1. Estude o capítulo «Introduções» (que atualizei esses dias).
2. Faça os homeworks anteriores que tem deixado pra lá!

Histórico de aulas

17/02/2020: Intro; U0

• ToC de FMC2
• Tipos (objeto vs proposição)
• atômicas vs compostas
• definições e teoremas
• noções primitivas e axiomas
• teorema, lemma, corolários, conjectura
• demonstrações como jogos e programação
• dados – alvos
• linhas de código vs comentários
• conectivos: como atacar e como usar
• números vs numerais vs dígitos
• gramáticas BNF
• Nats
• Recursão
• árvores sintácticas e linhas de inferência

19/02/2020: Provinha 0

21/02/2020: Erros comuns [video]

• Type error
• igualdade vs equivalência, com e sem «def»
• igualdade intensional vs extensional, sintáctica vs semântica
• Erro de semântica
• Diferença entre as duas frases:
  • «Se __A__, (então) __B__.»
  • «Como __A__, (logo) __B__.»
• Existêncial: como atacar
• Existêncial: como usar
• Três enunciados dum teorema: mesma coisa ou não?
• Universal: como atacar
• Implicação: como atacar
• Conjunção: como atacar
• Conjunção: como usar
• erros de caligrafia e tipografia
• «vírgula mágica», «para» seco, «com», «sendo», «setinha mágica», etc.
• secas equações
• «⇒» vs «logo»
• a redundância de «... é verdadeiro»
• O significado da palavra «equivalente» em matemática
• Um exemplo de demonstração e seu tabuleiro
• REPL
• linha de código vs comentário
• variáveis livres e ligadas
• «para algum» e CUIDADO
• escrevendo gerundiando qualquerando palavrando (wtf)
• «Calculamos»
• nomes desnecessários

28/02/2020: Demonstrações; Conjuntos

• Demonstrações
  • Erro: afirmação do conseqüente
  • duas maneiras que uma definição pode ser errada
  • (∃x∈A)[φ(x)] e (∀x∈A)[φ(x)] como açúcar sintáctico
  • linguagem e metalinguagem, variáveis e metavariáveis
  • (∃!x)[φ(x)] e (∃!x∈A)[φ(x)] como açúcar sintáctico
• Conjuntos
  • idéia informal (Cantor)
  • Noções primitivas: ser conjunto, pertencer (∈)
  • Tipos de objetos e como introduzi-los
  • Conjuntos como “black boxes”
  • Igualdade entre conjuntos: A=B
  • conjuntos homo- e hetero- gêneos
  • Cuidado: O uso de ⊂ na literatura
  • As relações binárias: =, ⊆, ⊇, ⊊, ⊋
  • ⊈ vs. ⊊
  • Notação
  • sinônimos de conjunto e convenções de fonts
  • Set comprehension (Set-builder notation)
  • Definindo o conjunto vazio: nossos deveres
  • Três predicados: Empty(–); Singleton(–); Universal(–)
  • Obrigação de definir notação (nome) para objeto: artigo definido vs. indefinido
  • Provas de existência & unicidade: «fight club»
  • hw: existência do conjunto vazio
  • hw: unicidade do conjunto vazio
  • O conjunto vazio (Ø)

02/03/2020: Conjuntos

• Existe único x tal que...
• Negação: empurrando pra dentro
• Reductio ad absurdum, LEM, dupla negação
• mais set-builder e açucar sintáctico
• variáveis livres e ligadas; sombreamento de variável; capturação de variável
• Singletons
• O conjunto universal
• Oito proposições sobre o Ø e um conjunto A
• Escolhendo a ordem de atacar teoremas
• {Ø} ≠ Ø

04/03/2020: Conjuntos

• limitações da linguagem da lógica proposicional e o que ganhamos na FOL
• termos
• definição de mais notações set-builder
• Erro comum: quantos elementos {x,y,z} tem?
• Cardinalidade |A| e primeiras propriedades
• Operações entre conjuntos e dois jeitos de defini-las
• As operações binárias: ∩, ∪, \, Δ
• diagramas de Venn e definições formais
• A operação unária de complemento: ~
• O operador Powerset (℘)
• Iterando o ℘ no Ø
• Cardinalidade de ℘A
• Generalizando as operações de união e intersecção: as operações unárias ⋂, ⋃
• Iterando o ℘ no Ø

06/03/2020: Conjuntos

• tese vs hipotese
• intensão vs extensão
• Intuição sobre os ⋂, ⋃, e ℘ e as {, }
• Iterando os ⋂ e ⋃ no Ø
• «por vacuidade»
• Tuplas: interface, black box, notação

07/03/2020, 09h15–13h45: Naturais; Recursão; Indução

aulas gravadas correspondentes:

1. [12/08/2019]
2. [14/08/2019]
3. [16/08/2019]
4. [19/08/2019]
5. [21/08/2019]

• Números vs numerais
• Linguagens: sintaxe e semântica
• Nat(urais): uma definição humana
• um acordo sobre afirmações com (meta)variáveis não declaradas
• voltando: variável vs metavariável
• Nat(urais): uma definição com gramática
• Nat(urais): uma definição com regras de inferência
• os valores canônicos de Nats
• função/operação vs construtor
• Igualdade
• cuidado: os «para todo» e «existe»
• Recursão
• 2+3=5
• Recursão vs tijolo
• Calculando a soma com recursão
• onde focar para reduzir?
• Multiplicação
• 2 · 3 = 6
• qual resultado incompleto é melhor?
• precedência e associatividade de operadores
• Θ. Associatividade da +
• tem como continuar a demonstração?
• escolhendo variáveis com «linhas»: x', x'', etc.
• o problema que temos demonstrando esse teorema
• a recursão foi no segundo argumento, então...
• «para ALGUM»
• Recursão – Indução: dois lados da mesma moeda
• Indução
• quando podemos usar indução
• indução informalmente
• Esqueçam a receitinha de 3 passos!
• Indução como regra de inferência
• «Base» e «Passo indutivo»
• a regra de indução na verdade é um esquema
• indução para demonstrar nosso teorema atual
• «hipótese indutiva»
• Como podemos continuar agora?
• presente da recursão vs presente da indução
• E se eu nem precisei usar a hipótese indutiva?
• Faz diferença se escolher usar indução mais cedo?
• recap: associatividade da +
• tentar começar «por indução»
• «por indução no z»
• podemos trocar quantificadores consecutivos da mesma forma
• discussão: comparação das duas demonstrações
• comparando as H.I.'s
• o que ganhamos
• Θ: + é comutativa
• lemmas em demonstrações
• comparação com programação
• subinduções
• lendo as H.I. «com palavras da rua»
• escopos e escolhas de variáveis
• escopos e as várias hipoteses indutivas
• entender no coração, com palavras da rua
• passo indutivo da segunda sub-indução
• usando o ` ≟ '
• adição, multiplicação, exponenciação, e depois?
• escolhendo nomes lindos para nossas variáveis

09/03/2020: Lógica; Conjuntos

• Lógica
  • Disjunção: como atacar e como usar
  • Lógica clássica vs intuicionista
  • LEM, LDN
  • Dicas para uns homeworks
• Conjuntos
  • Princípio de inclusão–exclusão
  • Princípio da adição
  • Cardinalidade de ℘A: como demonstrar a propriedade
  • Demonstração de inclusões e igualdades
  • Θ: C\(A∪B) = (C\A)∩(C\B)
  • tuplas como noções primitivas
  • tuplas como black boxes
  • Equações fundamentais de tuplas
  • igualdade de tuplas
  • projeções: π_i
  • implementação de tipo
  • Implementando de 3-tuplas
  • def'inho criminoso
  • Podemos definir n-tuplas para outros n's?
  • Produto cartesiano (×)
  • Cardinalidade do A×B: princípio da multiplicação
  • Definindo o Aⁿ informalmente

11/03/2020: Conjuntos

• Implementação-agnóstico
• n-Tuplas e Aⁿ
• O tipo de 1-tuplas
• O tipo de 0-tuplas
• A única 0-tupla: ()
• Seqüências
• outras notações
• de operação binária para n-ária
• de n-ária para ``seq-ária''
• União e Intersecção de seqüências de conjuntos
• Σ vs. ⋃
• Riemann's rearrangement theorem

13/03/2020: Prova 1.1; Conjuntos

• «Seja (x,y) em A×B.» Pode?
• Prova 1.1
• Exemplo: Os conjuntos Aₚ de todos os ancestrais da pessoa p, e Vₚ de todos os vilarejos do país p.
• Família indexada
• Traduzindo afirmações da linguagem natural para relações entre conjuntos e vice-versa
• Família indexada como generalização de n-tuplas e seqüências
• Produto cartesiano generalizado (de família indexada de conjuntos)
• Conjuntos disjuntos dois-a-dois («pairwise disjoint»): definição com e sem índices

16/03/2020: Sermão; Funções

• Sermão
  • Quando um «Seja k natural.» fica esquisito e idéia péssima.
  • Arbitrário?!
  • Umas dicas para problemas em seqüências de conjuntos, seus limites, etc.
• Funções
  • Conceito, notação
  • Setinhas com e sem bundas
  • Duas religiões sobre funções e seus black boxes
  • Igualdade
  • Diferença entre f(x) e f
  • int foo(int x). Qual o tipo da foo
  • regra de inferênca de tipo de função
  • O conjunto (A→B) (também denotado por B^A)
  • graph(f)
  • range(f)
  • aridade de função e uso de tuplas
  • Diagramas internos e externos
  • Igualdade extensional vs. intensional

Futuro (fluido)