Issues

• Induction along membership

  FormalizedFormalLogic/Foundation#1029 · Filter by author indiscernibles opened on Oct 3, 2026

• HierarchySymbol.PrenexSemiformula

  FormalizedFormalLogic/Foundation#1008 · Filter by author SnO2WMaN opened on Sep 28, 2026
  5

  

• Revival Provability Logic (plan)

  FormalizedFormalLogic/Foundation#958 · Filter by author SnO2WMaN opened on Sep 23, 2026
  

• Carneiro's Result in FFL

  set theory
  FormalizedFormalLogic/Foundation#947 · Filter by author SnO2WMaN opened on Sep 19, 2026
  1

• Slaman 2004

  arithmetic
  FormalizedFormalLogic/Foundation#930 · Filter by author iehality opened on Sep 13, 2026

• Fix provability predicate

  FormalizedFormalLogic/Foundation#924 · Filter by author iehality opened on Sep 10, 2026

• Reflexivility of $\mathsf{PA}$

  arithmetic
  FormalizedFormalLogic/Foundation#919 · Filter by author SnO2WMaN opened on Sep 9, 2026
  1

• Finite axiomatizability of $\mathsf{I}\Sigma_n$

  arithmetic
  FormalizedFormalLogic/Foundation#918 · Filter by author SnO2WMaN opened on Sep 9, 2026

• Add formalization.yaml

  documentation
  FormalizedFormalLogic/Foundation#911 · Filter by author SnO2WMaN opened on Sep 6, 2026
  

• Lyndon Interpolation Theorem via Hauptsatz

  FormalizedFormalLogic/Foundation#871 · Filter by author SnO2WMaN opened on Jul 25, 2026

• Executable proof-checking at V := ℕ

  FormalizedFormalLogic/Foundation#856 · Filter by author lividgreen opened on Jul 22, 2026
  1

• Quantifier Elimination

  FormalizedFormalLogic/Foundation#821 · Filter by author SnO2WMaN opened on Apr 16, 2026
  1

• On naming convention and file structure

  FormalizedFormalLogic/Foundation#809 · Filter by author iehality opened on Mar 9, 2026
  3

• Refine proof system of first-order logic

  FormalizedFormalLogic/Foundation#793 · Filter by author iehality opened on Feb 28, 2026
  

• Abstract Witness Comparison

  arithmetic
  FormalizedFormalLogic/Foundation#775 · Filter by author SnO2WMaN opened on Feb 20, 2026
  

• Shappiro's Epistemic Arithmetic

  arithmetic
  FormalizedFormalLogic/Foundation#734 · Filter by author SnO2WMaN opened on Feb 4, 2026

• On Semantics category

  FormalizedFormalLogic/Foundation#719 · Filter by author iehality opened on Jan 27, 2026
  3

• Niebergall Arithmetic

  arithmetic
  FormalizedFormalLogic/Foundation#706 · Filter by author SnO2WMaN opened on Jan 22, 2026

• Heyting Arithmetic

  arithmetic
  FormalizedFormalLogic/Foundation#702 · Filter by author SnO2WMaN opened on Jan 14, 2026

• Finite axiomatizability of $\mathsf{I}\Sigma_n$ and reflexivility of $\mathsf{PA}$

  arithmetic
  FormalizedFormalLogic/Foundation#701 · Filter by author iehality opened on Jan 14, 2026

• Second incompleteness theorem in terms of interpretation

  arithmetic
  FormalizedFormalLogic/Foundation#532 · Filter by author iehality opened on Sep 2, 2025

• Parson's theorem

  arithmetic
  FormalizedFormalLogic/Foundation#495 · Filter by author iehality opened on Aug 4, 2025

• Dialectica interpretation for intuitionistic arithmetic theories

  arithmetic
  FormalizedFormalLogic/Foundation#494 · Filter by author iehality opened on Aug 4, 2025

• Remove List.conj₂ and List.disj₂

  FormalizedFormalLogic/Foundation#347 · Filter by author SnO2WMaN opened on May 12, 2025
  1

• Pi_2-Sound is Sigma_1-Sound

  arithmetic
  FormalizedFormalLogic/Foundation#319 · Filter by author SnO2WMaN opened on Apr 9, 2025
  1