sep上搜了一下Parigot的free...

sep上搜了一下Parigot的free deduction，没什么地位，没有专门词条，在proof theoretical semantics里提了一下。free deduction也出现在Zach不久前的一篇非常丰富的natural deduction和sequent系统normalization的综述里，这篇论文涵盖了一个结论（类似nd）和多个结论（类似sequent）的情况。就是有个generalization的框架，符合框架的逻辑系统设计都能有cut elimination/normalization。

图片上free deduction的rule，只有propositional的，任何一个表达式出现在 ⊢ 左侧的可以理解false，右侧的理解为true，比如第一条，A and B false，A true，B true，这是contradiction。就这么一个简单的设计原则。conclusions里没有active formula了，只剩合并的context。（大括号里的公式表示它和括号左侧的公式是二选一）

先不说这个系统会具有什么特性，单单能基于truth-functional设计出这样的deduction系统，很叉吧。

FD是那个著名的能跑皮尔斯公理类型的call/cc的λμ calculus的泛化系统。