O método

Conceitos matemáticos se fixam quando atravessam representações — não quando são repetidos em exercícios. Axm parte dessa premissa. Três referências teóricas sustentam cada decisão editorial.

Registros de representação semiótica

Um objeto matemático não existe em uma única forma. Manifesta-se em quatro registros distintos:

Linguístico — sentenças em linguagem natural.
Simbólico — notação formal.
Gráfico — diagramas, figuras, gráficos.
Computacional — código que executa o objeto.

A formulação vem de Raymond Duval, pesquisador francês em didática da matemática, em Sémiosis et pensée humaine (1995). Duval parte de uma observação sobre a matemática que outras disciplinas não compartilham: seus objetos só são acessíveis por meio de signos. Ninguém tem experiência direta de um número, de uma função, de um espaço vetorial. Só há as representações que os referenciam. Cada registro é um sistema completo de signos, com sintaxe, regras de combinação e um critério para reconhecer quando dois signos referem ao mesmo objeto.

Compreensão real é a capacidade de converter entre registros — reconhecer o mesmo objeto sob signos diferentes. Quem domina apenas um registro manipula sinais sem alcançar o objeto. O salto cognitivo acontece na conversão, sobretudo quando a passagem entre registros não é trivial.

Duval distingue conversões congruentes das não-congruentes. Uma conversão é congruente quando preserva três propriedades:

Correspondência sinal-a-sinal — cada signo no registro de origem mapeia para um signo no registro de destino.
Univocidade terminal — o mapeamento é unívoco, sem ambiguidade no destino.
Ordem preservada — a ordem de leitura é a mesma em ambos os registros.

Quando as três valem, o leitor converte automaticamente, vê o mesmo objeto sem esforço.

A não-congruência é onde se concentra a maior parte da dificuldade pedagógica — e onde as explicações mais valiosas operam. A contrapositiva de $P \rightarrow Q$ se escreve $\neg Q \rightarrow \neg P$ . A ordem se inverte e a polaridade muda; o leitor precisa reconhecer que ambas dizem exatamente a mesma coisa, apesar do desencaixe sinal-a-sinal. Esses pontos são sinalizados explicitamente nos módulos do Axm, em vez de assumidos como óbvios.

Cada módulo trata os quatro registros como slots de autoria. Um conceito não está completo até ter sido articulado em pelo menos três registros dentro do mesmo módulo — regra editorial, não sugestão. Registros são lente de autoria, não scaffold de UI. Uma seção bem construída move-se entre eles naturalmente; a lente serve para verificar se o conceito de fato atravessou registros ou se ficou preso em um só.

Reificação

A formulação é de Anna Sfard, pesquisadora israelense em cognição matemática. Todo conceito matemático atravessa três estágios cognitivos antes de se fixar:

Interiorização — o leitor opera com objetos prévios, executando passos.
Condensação — os passos passam a ser tratados como um todo, sem precisar destrinchar.
Reificação — a operação se torna um objeto sobre o qual outras operações podem agir.

Reificação é o gargalo. Sem ela, o leitor calcula mas não manipula.

Cada conceito do Axm é apresentado em duas direções. Como processo, mostrando o que ele faz. Como objeto, mostrando o que outras coisas podem fazer com ele. Uma função é uma regra que age sobre entradas; também é uma entidade que se compõe, se inverte, se diferencia. Um conjunto é uma coleção; também é o argumento de união, interseção e produto.

O gatilho de reificação mais confiável é encontrar a formulação verbal certa — a frase que usa primitivas já reificadas pelo leitor. A maior parte do trabalho de autoria, quando funciona, é encontrar essas formulações.

Motivação semiótica antes da manipulação

Notação matemática não é arbitrária na maioria dos casos. Cada símbolo carrega a memória do que representa:

$\forall$ é um A invertido — de all.
$\exists$ é um E refletido — de exists.
$\sum$ é o Sigma grego — de sum.
$\int$ é o S longo medieval — de Summa, herança de Leibniz.
$\in$ é um epsilon estilizado — de esti, “é” em grego.
O blackboard-bold de $\mathbb{Z}\,\mathbb{Q}\,\mathbb{R}\,\mathbb{C}$ vem das iniciais — Zahlen, Quoziente, Reals, Complex.

Quando a iconicidade é conhecida, o símbolo se torna seu próprio mnemônico. Quando não é, ele permanece opaco no primeiro encontro e a cadeia de fixação quebra ali.

Um de nossos princípios editoriais é que todo símbolo introduzido é semioticamente motivado antes de ser operado.

Curry-Howard como ponte

A correspondência Curry-Howard estabelece uma equivalência formal entre lógica e teoria de tipos. Não é analogia pedagógica — é teorema, formulado por Haskell Curry nos anos 1930 e estendido por William Howard em The Formulae-as-Types Notion of Construction (1969). Cada construto do cálculo lambda tipado corresponde a um construto da dedução natural.

O dicionário cobre os conectivos centrais:

Proposições são tipos; provas são termos — programas habitando esses tipos; axiomas são constantes declaradas.
Condicional $P \rightarrow Q$ é o tipo de função de $P$ em $Q$ .
Conjunção $P \wedge Q$ é o tipo produto — uma tupla, um registro.
Disjunção $P \vee Q$ é o tipo união.
Verdadeiro é o tipo unitário; falso é o tipo vazio (Never em TypeScript, NoReturn em Python).
Modus ponens é literalmente aplicação de função.

Os quantificadores têm correspondentes mais elaborados. $\forall x.\, P(x)$ é o tipo de função dependente; $\exists x.\, P(x)$ , o par dependente. Aparecem em sistemas de tipos avançados como Coq, Lean e Idris; linguagens comerciais como Python e TypeScript não chegam até aí, mas cobrem toda a lógica proposicional.

Quem escreve código tipado está, na mesma sintaxe, escrevendo provas matemáticas. A função def implies(p: P) -> Q: ... é uma prova de $P \rightarrow Q$ ; a herança class A(B): é a relação de subconjunto; o union type P | Q é a união de conjuntos. Mesma sintaxe, dois nomes.

O Axm aproveita isso diretamente. O registro computacional, quando presente, não é uma analogia que ajuda a ver a matemática — é a matemática, em uma sintaxe que o leitor-programador já domina. Quem trabalha com tipos há anos já tem, sob outros nomes, as estruturas centrais da lógica formal reificadas. A correspondência é explicitada para que esse reconhecimento aconteça sem precisar duplicar o trabalho.

Geometria primeiro, quando aplicável

Fatos algébricos são apresentados através de representações geométricas sempre que a conversão é congruente. A distributividade aparece como um retângulo cortado; $(a + b)^2$ , como um quadrado decomposto em quatro regiões; Pitágoras, como composição de áreas. O registro geométrico é o ponto de entrada sempre que a reificação espacial chega mais rápido que a simbólica.