Carnap — Formal Logic in the Browser
by Graham Leach-Krouse, Jake Ehrlich · Carnap / Open Tower
Browser-based logic courseware that machine-checks propositional proofs line by line in Fitch, Kalish-Montague and Hardegree styles, plus truth tables, symbolization and truth trees. Instant feedback on exactly where a derivation breaks. Free and open source. Propositional logic is learned by doing proofs and being told precisely which line is wrong. Carnap is the only free tool that checks derivations across several standard proof styles rather than just evaluating truth tables, so it is the practice layer the textbooks need.
More resources on Propositional Logic
Wolfram MathWorld
MathWorld is an online mathematics encyclopedia from Wolfram Research offering detailed, browsable articles on topics across the math spectrum, including algebra, geometry, calculus, and number theory. Each entry includes definitions, theorems, formulas, diagrams, worked examples, and links to further reading.
plato.stanford.edu
The Stanford Encyclopedia of Philosophy is a peer‑reviewed online encyclopedia of philosophy featuring in‑depth, scholarly articles written and regularly updated by experts, including comprehensive coverage of logic topics.
forall x Open Logic Project
Free open-licensed textbook from the Open Logic Project, based on P.D. Magnus's forall x, teaching formal logic from truth-functional logic through first-order predicate logic, with natural deduction, translation exercises and semantics. Readers learn to symbolize English arguments and construct formal proofs.
Mathematics for Computer Science (MIT 6.042J)
Discrete mathematics for computer science with an emphasis on definitions and proofs: logic, induction, sets and relations, graph theory, modular arithmetic, asymptotics, counting and discrete probability. 25 lecture videos, problem sets and exams with solutions build fluency in writing proofs.
Propositional Logic (Stanford Encyclopedia of Philosophy)
Peer-reviewed survey of propositional logic. Covers truth-functional completeness, decidability and SAT, axiomatic and natural deduction systems, Gentzen sequent calculi, and proofs of completeness and compactness, then turns to many-valued, intuitionistic, relevance and linear logics. Covers the deeper metatheory the topic still lacks: completeness and compactness proofs, the proof systems compared, and non-classical variants. It is the step after the textbook and course.
Stanford Introduction to Logic
Free self-paced Stanford course with an online text, interactive exercises and a built-in Fitch proof editor. Covers propositional syntax and semantics, truth tables, satisfiability, validity, logical entailment and formal proofs, then moves on to relational logic. A structured course where learners get instant feedback on truth tables and proofs. It approaches logic from the computer-science side (satisfiability, entailment, circuits), which complements the philosophy angle of forall x and IEP.