邏輯經驗論者R. Carnap在1930年提到,雖然G. Frege的新邏輯出現已逾數十年,但是大部分的教科書仍未意識到新邏輯與Aristotle的舊邏輯有著根本上的差異。有趣的是經過數十年的發展,我發現古典邏輯的演算系統也出現相同情況,截至目前為止,大部分的教科書也未意識到樹枝法的重要性,主要原因在於雖然在限定的範圍中,樹枝法和真值表法同樣能夠提供證明可決定性的程序,卻無法如自然演繹法等以直接證法為主要證明策略的方法一般,呈現如何從前提逐步推論到結論的過程。但是,以直接證法為主要證明策略的演算系統而言,無論是公理法或自然演繹法,要建構這類演算系統的證明其實有個困難之處,因為這些演算系統並未提供如樹枝法般能夠有效率地找到證明的操作程序。不過,在這篇論文中,我要說明的是樹枝法不但具有找到證明的操作程序,而且透過樹枝法的原型,即E. W. Beth提出的語意真值圖,還能夠進一步建構自然演繹法的證明,如果透過Beth的方法能夠成功地建立樹枝法與其他以直接證法為策略的演算系統之間的轉換形式,那麼對於建構以直接證法為策略的演算系統的證明將會有相當大的助益。 The prominent empiricist R. Carnap mentioned in 1930 that most logic textbooks were still unaware of the essential difference between traditional logic and the new one though the latter has been developed for half century since G. Frege. It is surprising that the same situation happens today in calculus systems in classical logic. From an inferential point of view, these systems can be divided into two different main strategies, one is called direct proof as axiom system and natural deduction but the other is indirect as tableaux system. The advantage of indirect proof is to provide a decision procedure to decide whether an argument is valid or not. But on the other side, direct proof could represent the derivation step by step. What I am curious is it possible to combine these two advantages via transformation between different systems. So far, most textbooks of elementary logic presented these systems as independent to each other but I found it might be a way to connect indirect proof to direct one. In this essay, I suggest that Beth’s semantic tableaux method indeed inspired us to characterize the connection of two strategies of proof.