This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...) implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

Machine learning methods have been used in multifactor stock strategy for years. This paper uses three machine learning methods and linear regression method to find the most appropriate approach. First, a framework is established and 10 style factors and 30 industry factors are chosen. Second, four methods are used to forecast portfolio returns and compared by predicting returns, successful rate, and Sharpe ratio. Finally, this paper draws conclusion. The main findings are as follows: the support vector regression has the most (...) stable successful rate for predicting, while ridge regression and linear regression have the most unstable successful rate with more extreme cases; algorithm of support vector regression fitting higher-degree polynomials in Chinese A-share market is optimized, compared with the traditional linear regression both in terms of stock return and retracement control; the results of support vector regression significantly outperforming the CSI 500 index prove further. (shrink)

As the primary value system in Chinese culture for almost 2,000 years, Confucianism has profoundly influenced the mindset of Chinese people. Cultural psychology studies have highlighted that individuals with different cultural backgrounds vary in their preferences for certain personality traits, such as self-construal, and their metacognitive characteristics, such as thinking modes. Compared with Western cultures, Chinese culture shows a preference for the interdependent self and holistic thinking. To investigate the relationship between the relational-interdependent self, holistic thinking, and traditional Chinese values, (...) we surveyed 327 Chinese adults using the Confucian Traditional Values Survey, Holistic Thinking Scale, and Relational-Interdependent Self-Construal Scale. The results show that Confucian values positively influence both holistic thinking and the relational-interdependent self, the latter of which partially mediates the positive relationship between Confucian values and holistic thinking. This study deepens the understanding of the psychological features of Chinese culture. (shrink)